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 7 mai, 10h30

                             ------------------
                             Beniamino Accatoli
                             ------------------

                                    LIX

          =======================================================
          Abella formalization of lambda-calculus residual theory
          =======================================================

Abella is a new proof assistant developed by Andrew Gacek and based on
work of Gacek, Miller and Nadathur. Its main feature is a primitive
handling of binders via higher order abstract syntax and the nabla
quantifier. In the talk we introduce the system and present a
formalization of  the residual theory of lambda calculus. This
development is actually a re-formalization of a work of Huet in Coq.
Thanks to the features of  Abella and to a re-understanding of the
Huet's work we get an elegant and extremely concise formalization of
the cube lemma for residuals. We also discuss some work in progress
towards the formalization of more advanced results.