- Ankush Das
- Stephanie Balzer
- Stephen McIntosh
- Frank Pfenning
- Ishani Santurkar
- Bryan Parno
- Andrew Miller
Programming digital contracts comes with unique challenges, which include expressing and enforcing protocols of interaction, controlling resource usage, and tracking linear assets. Nomos is 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 linear assets, Nomos employs a linear type system that prevents assets from being duplicated or discarded. A main innovation is the design and soundness proof of Nomos’ type system, which integrates shared session types and resource-aware session types with a functional type system that supports automatic amortized resource analysis.
In part supported by NSF SaTC Grant 1801369.
Combining Source and Target Level Cost Analyses for OCaml Programs Working paper. 2020
Resource-Aware Session Types for Digital Contracts In 2021 IEEE Computer Security Foundations Symposium (CSF’21). 2021
Work Analysis with Resource-Aware Session Types In 33th ACM/IEEE Symposium on Logic in Computer Science (LICS’18). 2018