Newsgroups: fr.announce.seminaires
Distribution: fr
From: Christine.Paulin@lri.COUPER-MOI.fr
Organization: INRIA-Rocquencourt
Subject: SEM - INRIA : Coq - 4/12/98 - Paris - FR

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E
       ____               ____                             ___                
      /    _   _         /     __     __  /_  _   /       /   |  _   __   _   
     /    / \ / \  ___  /     /  | / /_  /   __| /  ___  /___/  __| /  | __|  
    |___  |_/ |_/      |____ /    / __/ |_  |_/ |_      /      |_/ /    |_/   
               /                                                              
              /                                                               
                          I N R I A - Rocquencourt, 
                       Salle de conference du Bat 11

                         Vendredi 4 decembre, 10h30

                     ----------------------------------
                      Martin Strecker and Marko Luther
                     Institution :  Universit\"{a}t Ulm
                     ----------------------------------


          =======================================================
          Proof construction in type theory - the Typelab  system
          =======================================================


This talk will discuss methods of interactive and automated proof construction
in type theory and present an implementation of these methods in the Typelab
system.

To facilitate proof construction in type theory, metavariables are introduced
as placeholders for proof objects. These metavariables can be further refined
or solved in the course of a proof, for example by application of proof
rules or by unification. Some problems resulting from a naive treatment of
metavariables will be sketched, such as loss of commutativity of instantiation
of metavariables and reduction and ill-typed terms resulting from
reduction. To deal with these problems, a calculus with explicit substitutions
will be presented. This calculus differs from most calculi with explicit
substitutions in that substitutions can only be attached to metavariables,
which leads to a preservation of properties like confluence and strong normalization.
It will be shown that this calculus is not only adequate
for interactive proof construction, but can easily be converted to a sequent
style formulation which can be exploited for automating proof search.

The second part of the talk will give a survey of the Typelab system, a proof
assistant based on type theory. The integration of the above calculus into
Typelab and, more generally, some questions of term representation will be
discussed. Typelab has been implemented in an object-oriented extension of
Common Lisp and, for example, uses a non-standard representation of binding
structures.