X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Findex.ldw.xml;h=c5004f36a57a76361bcd130e295deb83604937d9;hb=503426723b9fc786c69dc988d38726997ecb809a;hp=e37ac33b26f2a99b7f17f08097e27aab5e1d794d;hpb=25577a78cccba09974c91fcbfea770091a413382;p=helm.git diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml index e37ac33b2..c5004f36a 100644 --- a/helm/www/lambdadelta/web/home/index.ldw.xml +++ b/helm/www/lambdadelta/web/home/index.ldw.xml @@ -3,29 +3,29 @@ Foreword - 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 some previously published informal material. + as a set of machine-checked digital specifications. - This is the System logo: crux_177.png - (revised ). + This is the family logo: crux_177.png + (revised ). - + To view this site correctly, please select a font with Unicode support. For example "Lucida Sans Unicode" (it should be already installed on your system). @@ -37,44 +37,120 @@ 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: - - (2012). In JAR 49(3), pp. 427-451. + Formal metatheory of programming languages in the Matita interactive theorem prover + (2012). In Journal of Automated Reasoning, 49(3), pp. 427-451. Springer. M.E. Maietti: - + Consistency of the minimalist foundation with Church thesis and Bar Induction (2012). Submitted article. W. Ricciotti: - + Theoretical and implementation aspects in the mechanization of the metatheory of programming languages (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna. C.E. Brown: - - (2011). Typescript note. + Faithful Reproductions of the Automath Landau Formalization + (2011). Technical report. M.E. Maietti: - - (2009). In APAL 160(3), pp. 319-354. + A minimalist two-level foundation for constructive mathematics + (2009). In Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier. V. Rahili: - - (July 2007). Typescript note. + First Year Report: Realisability methods of proof and semantics with application to expansion + (July 2007). Technical report. + + + + + Disclaimer + + The systens of the λδ family 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. + + + + + Moreover, the systens of the λδ family related intentionally to + Lady Lambdadelta, + the Witch of Certainty of the sound novel + Umineko no Naku Koro ni. + +