X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Findex.html;h=b9897a4126aeeeeeeca03fa6193903110ecc128d;hb=286f7302d857a8a6674e1cf66fa1b1a1527dd1ac;hp=8a582d04c4bc8ae17bdaff2e8c444b7a9c8c9682;hpb=d966abb5707d0ce51be932b7bde99d4325d23a0c;p=helm.git diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 8a582d04c..b9897a412 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -16,12 +16,12 @@
- [lambdadelta home] + [\lambda\delta home]
The Formal Systems of the λδ (\lambda\delta) Family
- [Spacer] + [Spacer]

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,16 +95,14 @@ version 1 - helena - - -
+ library + (static LDDL directory)
-
Foreword [spacer] +
Foreword [spacer]
The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support @@ -128,7 +128,7 @@ "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
-
Citations [spacer] +
Citations [spacer]
This is a list of publications citing λδ documentation. @@ -136,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.
    @@ -172,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,18 +183,18 @@
-
Disclaimer [spacer] +
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. + 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 + λ-δ of A. Church: - The calculi of lambda-conversion + The calculi of lambda-conversion (1941). Annals of Mathematics Studies 6. Princeton University Press. @@ -202,9 +202,9 @@
  • - ∆Λ of + ∆Λ of N.G. de Bruijn: - Generalizing Automath by means of a lambda-typed lambda calculus + 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. @@ -212,10 +212,10 @@
  • - λ∆ + λ∆ of N.J. Rehof, M.H. Sørensen: - The λ∆-calculus + The λ∆-calculus (1994). In Lecture Notes in Computer Science, 789, pp. 516–542. Springer. @@ -223,9 +223,9 @@
  • - λ∆ of + λ∆ of S. Ronchi Della Rocca, L. Paolini: - The Parametric Lambda Calculus + The Parametric Lambda Calculus (2004). Texts in Theoretical Computer Science, An EATCS Series. Springer. @@ -233,25 +233,31 @@
  • - λD of + λD of R. Nederpelt, H. Geuvers: - Type Theory and Formal Proof + Type Theory and Formal Proof (2014). Cambridge University Press.
  • - Cλξ of + Cλξ of N.G. de Bruijn: - A namefree lambda calculus with facilities for internal definition of expressions and segments + A namefree lambda calculus with facilities for internal definition of expressions and segments (1978). TH-report 78-WSK-03. Eindhoven University of Technology, Eindhoven.
+
+ Moreover, the systens of the λδ family are not related intentionally to + the character Lady Lambdadelta, + the Witch of Certainty of the sound novel + Umineko no Naku Koro ni. +
- [Spacer] + [Spacer]

@@ -276,6 +282,6 @@

-
Last update: Wed, 30 Dec 2015 12:08:04 +0100
+
Last update: Fri, 08 Apr 2016 22:51:19 +0200