Sites Inria

English version

Séminaire des équipes de recherche

The PML₂ Language: Proving Programs in ML

© INRIA Sophie Auvin - G comme Grille

We present the PML₂ language, which provides a uniform environment for programming, and for proving properties of programs in an ML-like setting

  • Date : 8/03/2018
  • Lieu : Inria de Paris- 2 rue Simone Iff- 75012
  • Intervenant(s) : Rodolphe Lepigre - Inria Saclay, LSV, CNRS

The language is Curry-style and call-by-value, it provides a control operator (interpreted in terms of classical logic), it supports general recursion and a very general form of (implicit, non-coercive) subtyping. In
the system, equational properties of programs are expressed using two new type formers, and they are proved by constructing terminating programs.

Although proofs rely heavily on equational reasoning, equalities are exclusively managed by the type-checker. This means that the user only has to choose what equality to use, and not where to use it, as is usually done in mathematical proofs. In the system, writing proofs mostly amounts to applying lemmas (possibly recursive function calls), and to perform case analyses (pattern-matchings).

Mots-clés : Séminaire Gallium Inria de Paris PML₂ Language Proving Programs ML

Haut de page

Suivez Inria