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

Ciclo de workshops de promoção do bem-estar, relaxamento e criatividade.

Logótipo do evento, sobre um fundo branco

A Física Fora da Academia está de volta!

Fotografia da cidade de Grenoble, acompanhada do título e data do evento

Um evento com a participação de professores, funcionários, estudantes e membros da administração das sete Instituições de Ensino Superior que integram a Unite!, uma aliança de universidades europeias da qual faz parte a Universidade de Lisboa.

Mathematical Logic Webinar, por Isabel Oitavem (FCT - Universidade Nova de Lisboa).

Mosaico de fotografias, a preto e branco, de mulheres cientistas

O livro reúne mais de uma centena de retratos de investigadoras captados pelas objetivas dos fotógrafos Clara Azevedo, José Carlos Carvalho, Luís Filipe Catarino e Rita Carmo

Logótipo do LASIGE

RSS Meetup, por Diogo Poças (LASIGE, DI-FCUL).

Ciclo de webinars dedicado as desafios na conciliação da conservação.

Seminário do Departamento de Física de Ciências ULisboa, por Pavel Kroupa (University of Bonn & Charles University, Prague).

Imagem ilustrativa do evento, acompanhada de várias informações (título, data e hora do evento; orador)

52.º PubhD de Lisboa, por Cédric Pereira (Ciências ULisboa / IA - Instituto de Astrofísica e Ciências do Espaço).

Representação de diagrama

Submissão de candidaturas até 10 de março de 2021.

The workshop series aims to contribute to a broader debate on the relation between science and policymaking.

Ciclo de workshops de promoção do bem-estar, relaxamento e criatividade.

Logótipo do Dia Internacional da Matemática, sobre um fundo branco

O Departamento de Matemática de Ciências ULisboa preparou um conjunto de atividades especiais para celebrar o Dia Internacional da Matemática (IDM).

Título do evento, acompanhado da data e dos logótipos das entidades organizadoras

Iniciativa no âmbito das celebrações do Dia Internacional da Matemática.

Imagem ilustrativa do Doutoramento em História e Filosofia das Ciências

Provas de 2.º ano do Doutoramento em História e Filosofia das Ciências, por Sima Krtalic.

Seminário no âmbito da Unidade Curricular de Desenvolvimento de Produtos Funcionais, por Ana Cristina Gonçalves Monteiro (FeedInov CoLab).

Geometry Webinar, por Ricardo Campos (CNRS/University of Montpellier).

Logótipo do ciclo de webinars, sobre um fundo branco

At AppEEL, we aim to advance the study of evolution from an inter- and transdisciplinary approach and to identify how biological evolutionary theories can be applied to the epistemological, sociocultural and linguistic domains.

Seminário no âmbito da Unidade Curricular de Desenvolvimento de Produtos Funcionais, por André Filipe Lagoa Costa (Mandara Labs).

Logótipo do programa HiTech, acompanhado de informações úteis (objetivos e prazo de candidatura)

Candidaturas ao programa, destinado a capacitar investigadores na valorização dos resultados de investigação científica, a decorrer até 26 de março de 2021.

Imagem ilustrativa do evento, acompanhada de várias informações úteis (data/hora/local)

Um debate aberto ao público, especialmente indicado a quem se interroga sobre a Matemática e o seu futuro.

This course aims at exploring how scientists can use social media as tools to enhance the communication of their research and the dialogue with society, and discussing the differences that exist in the work of scientists and journalists in terms of the methods and deadlines they meet and exploring how scientists and journalists can better articulate.

This course will teach how to apply the SWAT eco-hydrological model to assess the impacts of climate and associated changes on water-soil-plant interactions, and consequences to water resources, soil erosion and nutrient cycles.

Geometry Webinar, por Pierre Schapira (Professor emeritus Sorbonne University).

Páginas