X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Findex.ldw.xml;h=9ebac8e8069440e00a9906da6ac5850e41aaa8e6;hb=d966abb5707d0ce51be932b7bde99d4325d23a0c;hp=d60da5f21e48f41878f5d5ff8830d7884c68dbb3;hpb=25893b01cb815cbd9a3b9684952bfc0f42c0739d;p=helm.git diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml index d60da5f21..9ebac8e80 100644 --- a/helm/www/lambdadelta/web/home/index.ldw.xml +++ b/helm/www/lambdadelta/web/home/index.ldw.xml @@ -3,25 +3,24 @@ Foreword - 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 ). @@ -82,5 +81,67 @@ (July 2007). Technical report. + + + Disclaimer + + 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. + +