Sites Inria

English version

Séminaire des Équipes de Recherche

Séminaire Cambium : 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
  • Lieu : Salle Jacques-Louis Lions 1
  • Intervenant(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.

Mots-clés : Digital Programming Inria de Paris Cambium Sciences Recherche Séminaire Contracts Équipe

Haut de page

Suivez Inria