Proofs of programs and subtyping in PML2

Carte non disponible

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

Catégories Pas de Catégories

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.

Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange