Sites Inria

Version française

Research Teams' Seminar

Cambium Seminar: Nomos, Resource-Aware Session Types for Programming Digital Contracts

© INRIA Sophie Auvin - C comme Cryptographie

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.

  • Date : 16/12/2019
  • Place : Conference Room Jacques-Louis Lions 1
  • Guest(s) : Jan Hoffmann, Carnegie Mellon University

To describe and enforce protocols, Nomos is based on shared binary session types that are rooted in linear logic. To control resource usage, it uses 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.

Jan Hoffmann is an Assistant Professor of Computer Science at Carnegie Mellon University and a member of the Principles of Programming (PoP) group. His mission is to discover beautiful mathematical ideas that have a real-world impact, shape the way programmers think, and help to create software that is more reliable, efficient, and secure. He is an expert in reasoning about quantitative properties of programs and known for the design and implementation of Resource Aware ML. His work has been supported by an NSF Career Award, a Google Faculty Award, and by a scholarship of the German National Academic Foundation (Studienstiftung). His CV and publication list can be found here.

Keywords: Research Team Contracts Seminar Research Sciences Cambium Inria de Paris Programming Digital