Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                             JEUDI 8 mars, 10h30

                               ----------------
                               Rodolphe Lepigre
                               ----------------

                           Inria Saclay, LSV, CNRS

                  =========================================
                  The PML₂ Language: Proving Programs in ML
                  =========================================

We present the PML₂ language, which provides a uniform environment for
programming, and for proving properties of programs in an ML-like setting.
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).