To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 30/03/09 - 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

                            Lundi 30 mars, 10h30

                            -------------------
                            Dimitris Vytiniotis
                            -------------------

                             Microsoft Research

              ===============================================
              Complete and Decidable Type Inference for GADTs
              ===============================================

GADTs have proven to be an invaluable language extension for ensuring data
invariants and program correctness. Unfortunately, they pose a tough problem
for type inference: we lose the principal types property, which is necessary
for modular type inference.

We present a novel and simplified type inference approach for local type
assumptions from GADT pattern matches. Our approach is complete and decidable,
while more liberal than previous such approaches.

(Joint work with Tom Schrijvers, Simon Peyton Jones, and Martin Sulzmann.)