To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 23/11/09 - Paris - FR

           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 - Rocquencourt
                         Amphi Turing du bâtiment 1

                          Lundi 23 novembre, 10h30

                            --------------------
                            Dimitrios Vytiniotis
                            --------------------

                             Microsoft Research

              ===============================================
              Towards a more expressive core language for GHC
              ===============================================

The core language of GHC is based on System F-omega, enriched with type
equality coercions with explicit proof witnesses. The soundness of this
language relies on the consistency of the top-level equality axioms, provided
originally by source user declarations, and translated to core by type
inference. In the presence of type system features such as type functions and
newtypes it turns out that the ``obvious'' translation of top-level
declarations to core may give rise to inconsistent axioms, which threaten
soundness. In this talk I will present recent progress in tackling this
problem by elaborating the existing core language to include type ``codes'' in
addition to types. This addition allows for the consistent translation of
source top-level declarations to core language axioms.

This is work in progress with Stephanie Weirich, Steve Zdancewic, and Simon
Peyton Jones.