Foreword

Foreword $\lambda\delta butterfly$

- 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).

@@ -129,16 +128,23 @@ "Tools" menu â "Internet Options" entry â "General" tab â "Fonts" button.

Citations

Citations $\lambda\delta butterfly$

- 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.

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 $\lambda\delta butterfly$ +

+ 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. +

+ 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. +

+ $\lambda\delta rainbow rule$

@@ -202,6 +282,6 @@

Last update: Wed, 02 Sep 2015 17:59:06 +0200

Last update: Fri, 08 Apr 2016 22:51:19 +0200