Institut de Mathématiques de Marseille, UMR 7373


Accueil >

Proofs of programs and subtyping in PML2

Jeudi 16 février 2017 11:00-12:00 - Rodolphe LEPIGRE - LAMA, Université de Savoie

Proofs of programs and subtyping in PML2

Résumé : 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.

JPEG - 13.2 ko
Rodolphe LEPIGRE

Lieu : Salle des séminaires 304-306 (3ème étage) - Institut de Mathématiques de Marseille (UMR 7373)
Site Sud
Campus de Luminy, Case 907
13288 MARSEILLE Cedex 9

Exporter cet événement

Pour en savoir plus sur cet événement, consultez l'article Séminaire Logique et Interactions