X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Findex.html;h=d14a8519b6aa71b2e20c14840f394d5caa195ec8;hb=f7d7f2459b3b0409be5f168822be3b836ccc929b;hp=14c812b5fe9dc93b1ec4d919a09b3fd65a9934e7;hpb=25577a78cccba09974c91fcbfea770091a413382;p=helm.git diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 14c812b5f..d14a8519b 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -19,11 +19,11 @@ [lambdadelta home] -
The Formal System λδ (\lambda\delta)
+
The Formal Systems of the λδ (\lambda\delta) Family
[Spacer]
-
+

@@ -36,18 +36,24 @@ news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - @@ -56,16 +62,20 @@ milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 - - (background - core - applications) - library + (static LDDL directory) @@ -74,42 +84,42 @@ visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 + helena - +
- - 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 +
+ 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).
-
- λδ is developed in the context of the +
+ The λδ family is developed within the Hypertextual Electronic Library of Mathematics - as a machine-checked digital specification - that is not the formal counterpart of some previously published informal material. + as a set of machine-checked digital specifications.
-
- This is the System logo: crux_177.png +
+ 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. @@ -117,64 +127,130 @@ To change the current font follow: "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
- - - -
Citations [spacer] + +
Citations [spacer]
-
- This is a list of publications citing λδ (not including our own). +
+ 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. 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 JAR 49(3), pp. 427-451. + (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). Typescript note. + (2011). Technical report.
          - -
            +
            • M.E. Maietti: A minimalist two-level foundation for constructive mathematics - (2009). In APAL 160(3), pp. 319-354. + (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). Typescript note. + (July 2007). Technical report. +
                • +
              + +
              Disclaimer [spacer] +
              +
              + The systens 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. +
                • +
              +
              [Spacer]
              @@ -200,6 +276,6 @@

              -
              Last update: Tue, 28 Oct 2014 17:45:56 +0100
              - +
              Last update: Fri, 01 Apr 2016 23:30:52 +0200
              +