\lambda\delta home page

$[\lambda\delta home]$

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

$\lambda\delta rainbow rule$

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

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

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

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

Notice for the user of Internet Explorer. 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). To change the current font follow: "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.

Citations $\lambda\delta butterfly$

This is a list of publications citing λδ documentation.

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.

$\lambda\delta rainbow rule$

Last update: Thu, 16 Feb 2017 12:23:36 +0100