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 21 juin, 10h30

                              ----------------
                              Brigitte Pientka
                              ----------------

                             McGill University

                  ========================================
                  Programming proofs with contexts and ...
                  ========================================

Beluga is an environment for programming and reasoning about formal
systems given by axioms and inference rules. It implements the
logical framework LF for specifying and prototyping formal systems
via higher-order abstract syntax. It also supports reasoning: the
user implements inductive proofs about formal systems as dependently
typed recursive functions.  A distinctive feature of Beluga is that
it not only represents binders using higher-order abstract syntax,
but directly supports reasoning with contexts.  Taken together these
features lead to a powerful language which supports writing compact
and elegant proofs.

In this talk, I will give a status update on our Beluga development
and discuss its unique features by implementing the proof for type
uniqueness for the simply-typed lambda-calculus. This example will
also serve as a comparison to other systems which support reasoning
about formal systems.