Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E

                   ______                __    _               
                  / ____/___ _____ ___  / /_  (_)_  ______ ___ 
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/ 

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                           Lundi 16 décembre, 10h30

                                 ------------
                                 Jan Hoffmann
                                 ------------

                          Carnegie Mellon University

    =====================================================================
    Nomos: Resource-Aware Session Types for Programming Digital Contracts
    =====================================================================

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
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.

Short bio:

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 at
http://www.cs.cmu.edu/~janh/