To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 13/06/08 - Paris - FR

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

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                            Vendredi 13 juin, 14h

                              ----------------
                              Jacques Garrigue
                              ----------------

                            Université de Nagoya

                        ============================
                        Proving OCaml's type system?
                        ============================

Objective Caml's type system is a complex beast. At its core are
structurally polymorphic types, with objects and variants, with also
labels and first class polymorphism. On top of that it has subtyping
and a typed module system. We report on experiments in proving
properties of the underlying specifications using Coq, namely
soundness of objects and variants, and some properties of a fragment
of subtyping.