Proofs of programs and subtyping in PML2

Rodolphe Lepigre
LAMA, Université de Savoie

Date(s) : 16/02/2017   iCal
11 h 00 min - 12 h 00 min

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.


Retour en haut 

Secured By miniOrange