Proofs of programs and subtyping in PML2
Rodolphe Lepigre
LAMA, Université de Savoie
https://lepigre.fr/
Date(s) : 16/02/2017 iCal
11h00 - 12h00
PML2 is an ML style programming language that has the peculiarity of embedding an equational theory over its own programs, into its type system. This enables the specification of program properties as types, and they are then proved by constructing (terminating) programs inhabiting these types. After introducing the concepts of PML2, its type system and its classical realisability model, I will discuss recent work on subtyping and the implementation of PML2.
Catégories
