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

                           MARDI 21 février, 14h30

                               ----------------
                               Pierrick Couderc
                               ----------------

                          OCamlPro & ENSTA ParisTech

                     ===================================
                     Verification of OCaml typing proofs
                     ===================================

During type inference, the OCaml compiler builds a type-annotated abstract
syntax tree that can be seen as a typing proof. Ideally, a program checking
the correctness of those typing proofs should implement the OCaml type
discipline, and proving the soundness of this program should establish the
soundness of the OCaml type system.

In this talk, I will describe my ongoing work in checking OCaml type-annotated
ASTs, and formalizing in Coq the type soundness of a subset of OCaml.