X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Findex.html;h=36ac7c63096ef24b6343ad1b1af97261a3596a7a;hb=348f1670b30f52db99187b2e92b45348e18ebbbe;hp=0f1ce23d7f78e558d402c078b482a6fdb758dcaf;hpb=f72807cb8834aa8991919e365b57d553e3674908;p=helm.git diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 0f1ce23d7..36ac7c630 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -16,12 +16,12 @@
- [lambdadelta home] + [\lambda\delta home]
-
The Formal System λδ (\lambda\delta)
+
The Formal Systems of the λδ (\lambda\delta) Family
- [Spacer] + [Spacer]

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,31 +95,28 @@ version 1 - helena - - -
+ library + (static LDDL directory)
-
Foreword [spacer] +
Foreword [spacer]
- The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support + 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).
@@ -129,7 +128,7 @@ "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
-
Citations [spacer] +
Citations [spacer]
This is a list of publications citing λδ documentation. @@ -137,15 +136,15 @@
  • C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi: - ELPI: fast, Embeddable, λProlog Interpreter - (2015). In proc. of LPAR 20. LNCS 9450, pp. 460-468. + 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.
    @@ -173,7 +172,7 @@
  • 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.
    @@ -183,8 +182,83 @@ (July 2007). Technical report.
+ +
Disclaimer [spacer] +
+
+ 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. +
    • +
+
+ [Smiling face] + Moreover, the systens of the λδ family are not related intentionally to + Lady Lambdadelta, + the Witch of Certainty of the sound novel + Umineko no Naku Koro ni. +
- [Spacer] + [Spacer]

@@ -209,6 +283,6 @@

-
Last update: Thu, 10 Dec 2015 16:13:46 +0100
+
Last update: Sun, 22 May 2016 15:25:26 +0200