The Formal Systems of the λδ (\lambda\delta) Family

Foreword

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 (MF)
and its predecessors.

The λδ family is developed within the
Hypertextual Electronic Library of Mathematics (HELM)
as a set of machine-checked digital specifications.

This is the family logo: crux_177.png
(revised 2012-09).

Notice:
to view this site correctly, please install fonts
supporting Unicode 7.0 (June 2014).
For instance Unifont Upper
or Symbola
or Noto Sans Symbols2.

Citations

This is a list of publications citing λδ documentation.

- Yaoshun Fu, Wensheng Yu: Formalizing Calculus without Limit Theory in Coq (2021). In Mathematics, 9(12), pp. 1377:1-1377:24.

- M. Weber: An extended type system with lambda-typed lambda-expressions (2020). In Logical Methods in Computer Science, 16(4), pp. 12:1-12:50.

- M. Weber: An extended type system with lambda-typed lambda-expressions (extended version) (2020). Technical report. Faculty of Computer Science, Technical University of Berlin.

- M.E. Maietti, S. Maschio: An extensional Kleene realizability semantics for the Minimalist Foundation (2015). In Leibniz International Proceedings in Informatics, 39, pp 162-186. Schloss Dagstuhl, Leibniz-Zentrum für Informatik.

- 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 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: Faithful Reproductions of the Automath Landau Formalization (2011). Technical report.

- M.E. Maietti: A minimalist two-level foundation for constructive mathematics (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). Technical report.

Disclaimer

The systems 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 systems of the λδ family are not related intentionally to
Lady Lambdadelta,
the Witch of Certainty of the sound novel
Umineko no Naku Koro ni.

lambdadelta.info

Last update: Mon, 14 Jun 2021 16:10:45 +0200