Rencontre, 14 décembre 2017

Programme

10:30 – 12:00

François Pottier (INRIA)

Invited talk: Looking back on Mezzo: experience and metatheory

Mezzo is (a proposal for) a programming language equipped with an expressive type-and-permission system. Like ML, it is a high-level programming language, equipped with algebraic data types, first-class functions, polymorphism, garbage collection, etc. Its main innovation, in comparison with ML, is its affine type-and-permission system, which does not just describe the structure of data, but controls who has permission to read or write, and allows types (and permissions) to evolve over time. In this talk, I would like to give an informal overview of Mezzo's main design principles, followed with a more technical look at Mezzo's metatheory. The proof of type soundness, which has been verified in Coq, is first carried out for a core affine lambda-calculus, then extended with three independent features, namely affine references, locks, and adoption-and-abandon.

• accompanying slides for F. Pottier's talk

14:00 – 15:00

Kenji Maillard (INRIA)

Invited talk: F*, from practice to theory

F* is a programming language as well as a proof-assistant putting a strong emphasis on practical verification of effectful programs. In order to enable the verification of security critical programs such as cryptographic primitives (HACL) or protocols (TLS in MiTLS), F provides a rich logic with dependent types and universes, an effect-based weakest precondition calculus and an smt-automation backend. In this presentation, we will present how these ingredients are used in actual program verification and then give an account of their metatheoretical aspects.

15:30 – 16:30

Jean Krivine (IRIF, Univ. Paris Diderot)

Invited talk: Incremental Update for Graph Rewriting