Rencontre, Dec. 14, 2017

Nous serons en amphi B (site Monod, 3ème étage)


10:30 – 12:00

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.

14:00 – 15:00
Kenji Maillard (INRIA)

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)