Nomos

Collaborators

• Ankush Das
• Stephanie Balzer
• Stephen McIntosh
• Frank Pfenning
• Ishani Santurkar
• Bryan Parno
• Andrew Miller

Overview

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.

Website

Nomos website and interface

Support

In part supported by NSF SaTC Grant 1801369.

Publications

1. Combining Source and Target Level Cost Analyses for OCaml Programs Stefan Muller, and Jan Hoffmann Working paper. 2020 [pdf]
1. Resource-Aware Session Types for Digital Contracts Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, and Ishani Santurkar In 2021 IEEE Computer Security Foundations Symposium (CSF’21). 2021 [pdf]
1. Work Analysis with Resource-Aware Session Types Ankush Das, Jan Hoffmann, and Frank Pfenning In 33th ACM/IEEE Symposium on Logic in Computer Science (LICS’18). 2018 [pdf]