Contribution  Bologna/LAMBDA-TYPES
                       ==================================

This directory contains a formalization in Coq of "lambda-delta", a
lambda-typed lambda-calculus with abbreviations.

Author & Date: Ferruccio Guidi
               Department of Computer Science, University of Bologna
               March 2005
E-mail : fguidi@cs.unibo.it
WWW    : http://www.cs.unibo.it/~fguidi

Installation procedure:
-----------------------

  To get this contribution compiled, type

    make 

  or

    make opt

  The main modules produced by the compilation are:

     LambdaDelta   provides the theory of the "lambda-delta" calculus
                   and its prerequisites

     Base          provides just the prerequisites (mainly some arithmetic
                   properties missing in the standard library of Coq)

Description:
------------

  The present work, which is meant to be improved in the future, contains 
  a formalization of the "lambda-delta" calculus, defined in "item notation"
  and with De Bruijn indices, and includes the proofs of some standard
  properties of this calculus. In particular the user will find:
  
  - Confluence of reduction
  - Generation lemma
  - Thinning lemma
  - Substitution lemma
  - Type Correctness
  - Type Uniqueness
  - Subject Reduction

  Other properties to be added in the future versions of this contribution
  include (but are not limited to):
  
  - Strong Normalization
  - Decidability of Type Inference and Type Checking

Further information on this contribution:
-----------------------------------------

  The latest version of this development is maintained in the CVS repository
  of the HELM project <helm.cs.unibo.it> and can be downloaded at: 
   
  www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/coq-contribs/LAMBDA-TYPES.tgz