helm/coq-contribs/LAMBDA-TYPES/README

   1
   2                        Contribution  Bologna/LAMBDA-TYPES
   3                        ==================================
   4
   5 This directory contains a formalization in Coq of "lambda-delta", a
   6 lambda-typed lambda-calculus with abbreviations.
   7
   8 Author & Date: Ferruccio Guidi
   9                Department of Computer Science, University of Bologna
  10                March 2005
  11 E-mail : fguidi@cs.unibo.it
  12 WWW    : http://www.cs.unibo.it/~fguidi
  13
  14 Installation procedure:
  15 -----------------------
  16
  17   To get this contribution compiled, type
  18
  19     make
  20
  21   or
  22
  23     make opt
  24
  25   The main modules produced by the compilation are:
  26
  27      LambdaDelta   provides the theory of the "lambda-delta" calculus
  28                    and its prerequisites
  29
  30      Base          provides just the prerequisites (mainly some arithmetic
  31                    properties missing in the standard library of Coq)
  32
  33 Description:
  34 ------------
  35
  36   The present work, which is meant to be improved in the future, contains
  37   a formalization of the "lambda-delta" calculus, defined in "item notation"
  38   and with De Bruijn indices, and includes the proofs of some standard
  39   properties of this calculus. In particular the user will find:
  40
  41   - Confluence of reduction
  42   - Generation lemma
  43   - Thinning lemma
  44   - Substitution lemma
  45   - Type Correctness
  46   - Type Uniqueness
  47   - Subject Reduction
  48
  49   Other properties to be added in the future versions of this contribution
  50   include (but are not limited to):
  51
  52   - Strong Normalization
  53   - Decidability of Type Inference and Type Checking
  54
  55 Further information on this contribution:
  56 -----------------------------------------
  57
  58   The latest version of this development is maintained in the CVS repository
  59   of the HELM project <helm.cs.unibo.it> and can be downloaded at:
  60
  61   www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/coq-contribs/LAMBDA-TYPES