Resource-Aware Session Types for Programming Digital Contracts - Jan Hoffmann
Workshop on Dependable and Secure Software Systems 2019
This talk presents Nomos, a programming language that has been designed from scratch to address the unique challenges of programming digital contracts: describing and enforcing protocols of interaction, controlling resource usage, and tracking linear assets. To describe and enforce protocols, Nomos is based on shared binary session types rooted in linear logic. To control resource usage, it uses resource-aware session types and automatic amortized resource analysis (AARA), a type-based technique for inferring resource bounds. To track linear assets, Nomos employs a linear type system that prevents assets from being duplicated or discarded. The talk reviews AARA and session types, highlights the main design choices, and illustrates the concepts with example contracts.