\lambda\delta home page

[lambdadelta home]

The Formal System λδ (\lambda\delta)

home	news	documentation	specification		implementation
foreword	milestones	version 2	version 2	(background - core - applications)	library
notice	citations	version 1	version 1		helena

Milestones [spacer]

July 2014. A new version of this site is online.

June 2014. First communication on λδ version 2.

December 2012. The character "_" is removed from the denomination "lambda_delta":
- The denomination "\lambda\delta" is used in λδ-related texts.
- The denomination "lambdadelta" is used in λδ-related identifiers.
- Permanent λδ URL acquired: http://lambdadelta.info/ (pointing at this site).

September 2011. The denomination "lambda-delta" changes to "lambda_delta":
- The character "-" is reserved in λδ textual syntax (recognized by "Helena 0.8.1").
- Eventually, the occurrences of the character "-" will be replaced by "_" in all λδ-related identifiers.
- In particular, this refactoring involves file names and path names.

April 2011. The specification of λδ version 2 and related topics is restarted in Matita 0.5.

December 2010. Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012).

November 2010. "Helena 0.8.1" is released.

September 2009. "Helena 0.8.0" is released and the λδ Digital Library is started.

June 2009. "Helena", a validator for λδ version 2, is available as a part of the HELM software.

September 2008. This site is online.

July 2008. First journal paper on λδ accepted for publication.

July 2008. First procedural reconstruction for Matita 0.5 of the λδ version 1 for Coq 7.3.1.

June 2008. The HTML pages of the specification of λδ version 1 for Matita 0.5 are online.

May 2008. The specification of λδ version 1 is dismissed.

March 2008. The specification of λδ version 2 is started with Coq 7.3.1 (false start).

September 2007. The specification of λδ version 1 for Matita 0.4 is online.

November 2006. λδ version 1 is released.

December 2005. First communication on λδ version 1.

May 2004. The specification of λδ version 1 is started with Coq 7.3.1.

Citations

Here 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.

Visibility [spacer]

June 2014. The Google search for "formal system lambda delta" gives 5 resources about λδ in the first 6 results.

June 2014. The Yahoo search for "formal system lambda delta" gives 4 resources about λδ in the first 5 results.

[Valid XHTML 1.1]

[Valid CSS level 2]

[Generated from XML via XSL]

[PNG used here]

[Viewable with any browser]

Last update: Mon, 20 Oct 2014 16:37:19 +0200