SCS Seminar Talk: Ankush Das

TITLE: Programming Language Principles for Distributed Systems

ABSTRACT:

With the proliferation of distributed systems, the design of safe, secure, and efficient software has become an ever more complex task. The heterogeneous nature of these distributed systems have further introduced domain-specific programming requirements such as programming in an adversarial setting and inferring execution cost. Recognizing these requirements, my research has focused on advancing programming languages to support developers with program verification techniques, complexity analysis tools, and domain-specific languages.

In this talk, I focus on the domain of smart contracts, i.e., programs that enforce digital transactions, often legal or financial, between multiple parties. Programming smart contracts comes with its unique challenges, which include enforcing protocols of interaction, analyzing execution cost, and tracking linear assets. To address these challenges, the talk introduces Nomos, a programming language for smart contracts. To express and enforce protocols, Nomos is based on session types rooted in linear logic. To predict execution cost, Nomos uses resource-aware session types and automatic amortized resource analysis, a type-based technique for inferring cost bounds. To track assets, Nomos employs a linear type system that prevents assets from being duplicated or discarded.

The talk concludes with my future plans on exploring how programming languages can aid in the synthesis of smart contracts, verification of cryptographic protocols, and analysis of probabilistic systems with applications in artificial intelligence.

BIO:

Ankush Das is a final-year Ph.D. student at Carnegie Mellon University. He is advised by Professor Jan Hoffmann and closely works with Professor Frank Pfenning. He is broadly interested in programming languages with a specific focus on program verification, complexity analysis, and domain-specific languages. He is the lead designer and developer of Nomos, a programming language for smart contracts rooted in resource-aware session types. He has also designed the Rast language based on refinement session types that won the best system description paper award at FSCD 2020. Before joining CMU, he worked as a Research Fellow at Microsoft Research, India where he designed static analysis and verification tools for Windows driver modules. He completed his undergraduate at IIT Bombay, India in 2014 where he worked on deciding termination of linear loop programs.

JOIN THE TALK HERE: https://bluejeans.com/946032411