\lambda\delta home page

$[\lambda\delta home]$

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

$\lambda\delta rainbow rule$

Foreword $\lambda\delta butterfly$

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.

The current specification: λδ-2B for for Matita 0.99.4 (revised: 2020-12). Documentation (J2a).
The current specification depends on: λδ-ground for Matita 0.99.2 (revised 2020-12).

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.

[Official bronze sponsor of Unicode Consortium]

Citations $\lambda\delta butterfly$

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

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

If this image is not visible, forwarding is out of order.

$\lambda\delta rainbow rule$

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

home	news	specification	specification log		documentation	implementation
foreword	milestones	version 2	(background - syntax - core - applications)		version 2	helena	Open Symbolic Notation (OSN)
citations	visibility	version 1	(background - core)	(static HELM directory)	version 1	library	(static LDDL directory)