To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 22/01/07 - Paris - FR

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

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

                          Lundi 22 janvier, 10h30

                               -------------
                               Adam Chlipala
                               -------------

                     University of California, Berkeley

                 =========================================
                    A Certified Type-Preserving Compiler
                 from Lambda Calculus to Assembly Language
                 =========================================

I will present work on using the Coq proof assistant to build a certified
compiler for a tiny, statically-typed functional language. Following past work
in type-preserving compilation, each intermediate language of the compiler
preserves some type information, leading up to programs in an idealized
assembly language that contain enough meta-data to support nearly tag-free
garbage collection. The compiler is "certified" in the sense that it is proven
that any output of the compiler terminates with the same final result as the
corresponding source program. I give all of the source, target, and
intermediate languages denotational semantics, a choice known to interact well
with correctness proofs about code transformations. My encoding uses dependent
types to make it possible for every object language term to be translated into
a "native" Coq term, facilitating the use of Coq's definitional equality to
subsume many common types of reasoning. I will demonstrate this by showing how
simple automatic decision procedures are able to discharge almost all proof
obligations that arise in certifying some common stages of functional language
compilers.