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

O evento pretende reunir investigadores que trabalhem sobre temas ligados à indústria e sobre património técnico e industrial, para uma reflexão prospetiva sobre o património industrial e atuais vias de colaboração no seu estudo, salvaguarda e preservação.

Computador portátil a projetar imagem de sequência biológica

O curso visa a aquisição de conhecimentos sobre as ferramentas bioinformáticas disponíveis para efetuar análises de sequências de DNA e proteínas, bem como a autonomia e espírito crítico na utilização dessas ferramentas. Procura igualmente desenvolver competências na utilização de software de bioinformática disponível gratuitamente na Internet e na interpretação do significado biológico dos resultados.

Bola de cristal colocada no solo

O curso tem como objetivo apresentar aos participantes um estado da arte atualizado sobre a diversidade da biota do solo e os papéis funcionais desempenhados pelos organismos do solo nos principais processos ecológicos.

A conferência visa reunir os principais especialistas no domínio da Imagiologia Médica por Micro-ondas (MMWI) e incluirá palestras, apresentações e pósteres de resumos revistos por pares e artigos de conferências, bem como workshops em áreas satélite de investigação com interesse para a investigação em MMWI.

Páginas