X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Findex.html;h=b0c4d0792ae3e0247566ee0d36342216b39405a9;hb=ede1e31f13510c51d42d7b0448d3cbff132ec70c;hp=317de931de474ab0f75b518235824c941c253c97;hpb=d1ab998b8c8dacdfceee97d6275955675cf8be83;p=helm.git
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 317de931d..b0c4d0792 100644
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -19,7 +19,7 @@
-
- The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
- the foundations of Mathematics that require an underlying specification language
- (for example the
Minimal Type Theory
+ The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support
+ the foundational frameworks for Mathematics that require an underlying specification language
+ (for example the
Minimalist Foundation
and its predecessors).
- λδ is developed in the context of the
+ The λδ family is developed within the
Hypertextual Electronic Library of Mathematics
- as a machine-checked digital specification
- that is not the formal counterpart of previous informal material.
+ as a set of machine-checked digital specifications.
- This is the System logo:
crux_177.png
+ This is the family logo:
crux_177.png
(revised
2012-09).
@@ -132,13 +131,20 @@
Citations
- This is a list of publications citing λδ (not including our own).
+ This is a list of publications citing λδ documentation.
+
+ -
+ C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
+ ELPI: fast, Embeddable, λProlog Interpreter
+ (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer.
+
+
-
A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
Formal metatheory of programming languages in the Matita interactive theorem prover
- (2012). In JAR 49(3), pp. 427-451.
+ (2012). In Journal of Automated Reasoning, 49(3), pp. 427-451. Springer.
@@ -159,21 +165,89 @@
-
C.E. Brown:
Faithful Reproductions of the Automath Landau Formalization
- (2011). Typescript note.
+ (2011). Technical report.
-
M.E. Maietti:
A minimalist two-level foundation for constructive mathematics
- (2009). In APAL 160(3), pp. 319-354.
+ (2009). In Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier.
-
V. Rahili:
First Year Report: Realisability methods of proof and semantics with application to expansion
- (July 2007). Typescript note.
+ (July 2007). Technical report.
+
+
+
+
Disclaimer
![lambdadelta butterfly [spacer]](http://lambdadelta.info/images/b9.png)
+
+
+ The systens of the λδ family are not related intentionally to any other system
+ having (variations of) the symbols λ and δ in its name or syntax.
+ Examples include (but are not limited to):
+
+
+ -
+ λ-δ of
+ A. Church:
+ The calculi of lambda-conversion
+ (1941).
+ Annals of Mathematics Studies 6.
+ Princeton University Press.
+
+
+
+ -
+ âÎ of
+ N.G. de Bruijn:
+ Generalizing Automath by means of a lambda-typed lambda calculus
+ (1987).
+ In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
+ Marcel Dekker.
+
+
+
+ -
+ λâ
+ of
+ N.J. Rehof, M.H. Sørensen:
+ The λâ-calculus
+ (1994).
+ In Lecture Notes in Computer Science, 789, pp. 516â542.
+ Springer.
+
+
+
+ -
+ λâ of
+ S. Ronchi Della Rocca, L. Paolini:
+ The Parametric Lambda Calculus
+ (2004).
+ Texts in Theoretical Computer Science, An EATCS Series.
+ Springer.
+
+
+
+ -
+ λD of
+ R. Nederpelt, H. Geuvers:
+ Type Theory and Formal Proof
+ (2014).
+ Cambridge University Press.
+
+
+
+ -
+ Cλξ of
+ N.G. de Bruijn:
+ A namefree lambda calculus with facilities for internal definition of expressions and segments
+ (1978).
+ TH-report 78-WSK-03.
+ Eindhoven University of Technology, Eindhoven.
@@ -202,6 +276,6 @@
-
Last update: Sat, 21 Feb 2015 23:38:38 +0100
+
Last update: Wed, 30 Dec 2015 14:56:06 +0100