2 Contribution Bologna/LAMBDA-TYPES
3 ==================================
5 This directory contains a formalization in Coq of "lambda-delta", a
6 lambda-typed lambda-calculus with abbreviations.
8 Author & Date: Ferruccio Guidi
9 Department of Computer Science, University of Bologna
11 E-mail : fguidi@cs.unibo.it
12 WWW : http://www.cs.unibo.it/~fguidi
14 Installation procedure:
15 -----------------------
17 To get this contribution compiled, type
25 The main modules produced by the compilation are:
27 LambdaDelta provides the theory of the "lambda-delta" calculus
30 Base provides just the prerequisites (mainly some arithmetic
31 properties missing in the standard library of Coq)
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:
41 - Confluence of reduction
49 Other properties to be added in the future versions of this contribution
50 include (but are not limited to):
52 - Strong Normalization
53 - Decidability of Type Inference and Type Checking
55 Further information on this contribution:
56 -----------------------------------------
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:
61 www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/coq-contribs/LAMBDA-TYPES