\lambda\delta home page

The Formal System λδ (\lambda\delta)

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

Foreword

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 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 λδ (not including our own).

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

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

Last update: Tue, 20 Jan 2015 18:38:59 +0100