contribution about \lambda-\delta

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / README

diff --git a/helm/coq-contribs/LAMBDA-TYPES/README b/helm/coq-contribs/LAMBDA-TYPES/README
new file mode 100644 (file)
index 0000000..d35c2dd
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/README
@@ -0,0 +1,61 @@
+
+                       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