X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Findex.html;h=c8641b1cb8bbf96a5eac6dcfc6b97572bb1b1fde;hb=a3ab07c97eaea90a6f243f2053fb55151ecc12df;hp=20833265c179d4cbf59bacb04b904edf263036db;hpb=325319a6c28fd8c3992cdb0be745b0c7ca8651c3;p=helm.git diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 20833265c..c8641b1cb 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -23,156 +23,160 @@
[Spacer]
-
+

- - - - - - - + - - - - - - + - + - - - - - - + + -
- foreword + + home + news + documentation - implementation + + specification +
+
+ + implementation +
-
+ 		+ foreword -
- 		-
+ 		+ milestones - Version 2 + + version 2 - Background + + version 2 - Core + (background - core - applications) +
- Applications + + library (static LDDL directory)
-
+ 		+ citations -
+ 		+ visibility -
+ 		+ version 1 - Version 1 + + version 1 -
- 		-
+ 		(core)(static HELM directory) + helena +
- -
Foreword [spacer] +
Foreword [spacer]
-
+
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 some previously published informal material. + that is not the formal counterpart of previous informal material.
-
- λδ comes in several versions listed in the following table, - which includes the major milestones: +
+ This is the System logo: crux_177.png + (revised 2012-09).
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
versionnamedeveloped withstartedannouncedreleaseddismissed
2 - basic_2 - - Matita 0.99.2 - April 2011July 2014Planned in 2014Not planned yet
1 - basic_1 - - Coq 7.3.1 - May 2004January 2006November 2006May 2008
-
- -
Notice for the Internet Explorer user [spacer] -
-
+
+ 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 [spacer] +
+
+ 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. +
    • +
+
[Spacer]
@@ -198,6 +202,6 @@

-
Last update: Mon, 07 Jul 2014 23:14:51 +0200
- +
Last update: Mon, 19 Jan 2015 23:52:51 +0100
+