Login
Talks & Seminars
Title: Resource-Aware Session Types for Digital Contracts
Mr. Ankush Das, Carnegie Mellon University
Date & Time: May 14, 2019 11:00
Venue: Department of Computer Science and Engineering, Room No. 109, 01st Floor, New CSE/CC Building
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 two analyses for statically deriving worst-case bounds on the sequential (work) and parallel (span) complexity of message-passing processes, respectively. The work 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 span analysis enriches session types with temporal modalities to additionally prescribe the timing of the exchanged messages in a way that is precise yet flexible. The talk finally 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.
Speaker Profile:
Ankush Das is a fourth 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 analysis of resource consumption of programs. 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. Recently, he has been working with Stephanie Balzer, along with Prof. Frank Pfenning and Prof. Jan Hoffmann on designing Nomos, a type safe domain-specific programming language based on resource-aware session types for implementing smart contracts. 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 my undergraduate at IIT Bombay, India in 2015 where he worked with Prof. Supratik Chakraborty and Prof. Akshay S on deciding termination of linear loop programs.
List of Talks

Webmail

Username:
Password:
Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback