\lambda\delta home page

The Formal System λδ (\lambda\delta)

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

Foreword

The formal system λδ (\lambda\delta) is a typed λ-calculus 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 Hypertextual Electronic Library of Mathematics as a machine-checked digital specification that is not the formal counterpart of previous informal material.

This is the System 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

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. LNCS 9450, pp. 460-468.

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.

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 APAL 160(3), pp. 319-354.

V. Rahili: First Year Report: Realisability methods of proof and semantics with application to expansion (July 2007). Technical report.

Last update: Thu, 10 Dec 2015 16:13:46 +0100