Talks@LASIGE

Resource-Aware Session Types for Digital Contracts

Transmissão através de Videoconferência

Speaker: Ankush Das (Carnegie Mellon University).

Abstract: While there exist several successful techniques for supporting programmers in deriving static resource bounds for sequential code, analyzing the resource usage of message-passing concurrent processes poses additional challenges. To meet these challenges, this talk presents an analysis for statically deriving worst-case bounds on the computational complexity of message-passing processes, respectively. The analysis is based on novel resource-aware session types that describe resource contracts by allowing both messages and processes to carry potential and amortize cost. The talk then applies session types to implement digital contracts. Digital contracts are protocols that describe and enforce execution of a contract, often among mutually distrusting parties. Programming digital contracts comes with its unique challenges, which include describing and enforcing protocols of interaction, analyzing resource usage and tracking linear assets. The talk presents the type-theoretic foundations of Nomos, a programming language for digital contracts whose type system addresses the aforementioned domain-specific requirements. To express and enforce protocols, Nomos is based on shared binary session types rooted in linear logic. To control resource usage, Nomos uses resource-aware session types and automatic amortized resource analysis, a type-based technique for inferring resource bounds. To track assets, Nomos employs a linear type system that prevents assets from being duplicated or discarded. The talk concludes with future work directions on designing an efficient implementation for Nomos and making it robust to attacks from malicious entities.

Bio: Ankush Das is a final year PhD student at Carnegie Mellon University. He is advised by Prof. Jan Hoffmann. He is broadly interested in programming languages with a specific focus on resource analysis, session types and language design for smart contracts on the blockchain. He is the lead designer and developer of Nomos, a domain-specific language for implementing smart contracts based on resource-aware session types. In the past, he has worked jointly with Prof. Frank Pfenning and his advisor on designing resource-aware session types for parallel complexity analysis of concurrent programs implemented in a programming language called Rast. Before joining CMU, he worked as a Research Fellow at Microsoft Research, India with Akash Lal where he developed an efficient method to perform precise alias analysis for C and C++ programs for Windows driver modules to automatically infer safe null pointer dereferences. He completed his undergraduate at IIT Bombay, India in 2014 where he worked with Prof. Supratik Chakraborty and Prof. Akshay S on deciding termination of linear loop programs.


Zoom link

15h00
LASIGE

Seminário do Instituto de Astrofísica e Ciências do Espaço, por Pier-Stefano Corasaniti (Observatoire de Paris-Meudon, France).

Seminário de Lógica Matemática, por Antonio Piccolomini D'Aragona (University of Tübingen/University of Siena).

Seminário do Centro de Física Teórica e Computacional, por Hugo Terças (Departamento de Física do Instituto Superior de Engenharia de Lisboa, Instituto Politécnico de Lisboa / Instituto de Plasmas e Fusão Nuclear, Instituto Superior Técnico, Universidade de Lisboa, Portugal).

Um programa estruturado que combina discussões em grupo, exploração de carreira e workshops informativos, com inscrições até 23 de maio.

Uma oportunidade para fortalecer a cultura de segurança e bem-estar em CIÊNCIAS.

Logótipo do EVM 2025

O objetivo é proporcionar a estudantes de todo o país - que estejam a concluir o 2.º ou 3.º ano de licenciaturas em Matemática, Física ou áreas afins - a oportunidade de participar num projeto de investigação com a duração de duas semanas - candidaturas até 28 de maio.

Seminário no âmbito do Doutoramento em Biologia e Ecologia das Alterações Globais, por Pierina Jocelyn Mendoza Yengle.

Cartaz do filme "O Melhor dos Mundos"

A 29 de maio o filme "O Melhor dos Mundos” é exibido numa sessão especial em CIÊNCIAS, promovida pela FCiências.ID e o Instituto Dom Luiz. Após a projeção do filme, realiza-se uma mesa redonda com quatro especialistas em Sismologia, que responderão a perguntas do público.

Uma oportunidade única para interagir com a comunidade global de computação científica.

Logótipo Moodle

Ação de formação para docentes e investigadores de CIÊNCIAS.

Copilot Chat

Nesta sessão, serão exploradas as funcionalidades e benefícios do Microsoft 365 Copilot Chat de forma personalizada à comunidade académica de CIÊNCIAS.

Logótipo Mentimeter

Ação de formação para docentes e investigadores de CIÊNCIAS.

Luís Saraiva (Ciências ULisboa) é o coordenador nacional do evento.

Título/data/local do evento e iconografia representativa de energias renováveis

Junta-te a esta revolução energética e faz a diferença!

Comemoração do Dia Mundial da Segurança dos Alimentos em CIÊNCIAS.

Neste curso ficarás a saber como te podes tornar um permacultor eficiente, produtivo e consciente! O curso está preparado para iniciantes na prática de permacultura.

Formação - Cultivar em Permacultura.

Pessoas a interagirem em frente a um computador portátil

As inscrições para a edição de 2025 da formação decorrem até às 17h do dia 23 de maio.

Químico a escrever fórmulas num quadro

Curso acreditado para efeitos de progressão na carreira dos professores do Ensino Básico e Secundário do Grupo 510 (CCPFC/ACC-118288/22), com candidaturas até 18 de maio.

Curso destinado a estudantes de Mestrado e de Doutoramento, bem como a profissionais que desenvolvam investigação científica na área da saúde.

Título/data/local do evento e fotografia do mar

Quais são os conceitos-chave para enfrentar os atuais desafios marinhos e costeiros? 

Representação de programação R

This course aims at providing students with basic knowledge of R programming, allowing them to manipulate and visualize data with R.

The conference focuses on "Algebra and its role in Computer Science", with special emphasis on the areas of study related to the work of M. V. Volkov, such as semigroups and automata.

Logótipo do Verão na ULisboa, sobre um fundo azul

Candidaturas a partir de 07 de abril!

Título/data/local do evento e fotografia do espaço

How far will you go? The IA Summer Program 2025 is your launchpad to the Universe - apply until 26 May!

Páginas