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


In this course we will provide advanced hands-on training on some of the most used technological tools in field biology.

Inscrições abertas até 6 de junho.

Seminário Permanente de Filosofia das Ciências, por Vinícius Jonas de Aguiar (CFCUL/GI3).

E3 Talk, por Simone Vieira (Núcleo de Estudos e Pesquisas Ambientais, UNICAMP).

Título e data do evento, sobre fotografia de paisagem polar

Neste evento, a elite mundial de exploradores e cientistas partilhará com o público as descobertas mais recentes, as tecnologias mais inovadoras e as novas missões que prometem revolucionar o futuro do espaço, dos oceanos e do planeta.

A joint organization between Luisa Fiorot (Dipartimento di Matematica ”Tullio Levi-Civita”, Padova, Italy) and Teresa Monteiro Fernandes (CMAFcIO, FCUL, Portugal).

A short course by Luisa Fiorot (Dipartimento di Matematica ”Tullio Levi-Civita”, Padova, Italy).

Fotografia do mar, titulo dos cursos e logótipos das entidades promotoras

Brevemente serão disponibilizados mais 6 cursos, estando já previsto um na área da Biotecnologia Marinha, programado para início de outubro.

Título do evento e representação de átomo

O principal objetivo desta formação é capacitar doutorandos e doutorados de instituições de ensino superior e centros de investigação para os temas de empreendedorismo, inovação e transferência de conhecimento, permitindo-lhes perceber de que forma podem potenciar ainda mais o impacto gerado pelo

Colóquio de Matemática, por Jean-Baptiste Casteras (CMAFcIO, FCUL).

Sessão no âmbito do Lisbon Workshop Series.

Ação de formação para docentes, por Sofia Sá.

Título do evento e fotografia de participantes numa sessão

O prazo de submissão de resumos termina no dia 30 de abril.

Logótipo da iniciativa e fotografia de dois investigadores

Ciência Aberta e Inovação: uma abordagem colaborativa, transparente e acessível.

Título do evento e fotografia de dois estudantes

Candidaturas para estudantes regulares da ULisboa até 28 de março de 2023.

Título do evento e fotografia de utilizador de computador

Curso com candidaturas a decorrer.

Logótipo do prémio

As candidaturas à 10.ª edição decorrem até 30 de junho de 2023.

Título/data do evento, logótipo da Rede MAR e fotografia do mar

Applications from 01 June to 15 June 2023.

As candidaturas estão abertas até 26 de maio de 2023.

Logótipo do programa, sobre um fundo amarelo

Inscrições para Monitores até 31 de maio.

Título da iniciativa e fotografia do espaço

The program involves developing a research or science communication project under the supervision of researchers and science communicators from the Institute of Astrophysics and Space Sciences (IA). Two science communication workshops and a final seminar, in which the work developed is presented, are also part of the program.

Logótipo do CFTC, título e datas dos estágios

Three-weeks working on a project with a Researcher as a Supervisor, along with other workshops and activities - open to BSc or MSc students in Physics, Engineering Physics, Biomedical Engineering or other related fields.​

The course aims at enabling the participants to use different methods to measure the impacts of pollutants on ecosystems. Basic knowledge will be provided through theoretical and practical lessons on how to select and use the most suitable metrics based on the analysis of multiple compartments of the ecosystems.

Ação de formação para docentes, por Carlos Seco.

This course offers an overview of the different ways to measure biodiversity, and provides tips for the stratification of primary biodiversity data and the construction of variables that describe its various facets. It also includes an in-depth review of the different types of data used to measure biodiversity and their problems and limitations.