+
+ ![[\lambda\delta home]](http://lambdadelta.info/images/crux_32.png "\lambda\delta home")
+
+
+
+
+ cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
+
+ ![[Spacer]](http://lambdadelta.info/images/rainbow.png "\lambda\delta rainbow rule")
+
+
+
+
+
+ +
+
+
+
+
+ | + home + | ++ news + | ++ specification + | +
+ + |
+
+ + |
+ + documentation + | ++ implementation + | +
+ + |
+
| + foreword + | ++ milestones + | ++ version 2 + | +(background - core - applications) | +
+ + |
+ + version 2 + | ++ helena + | ++ Open Symbolic Notation (OSN) + | +
| + citations + | ++ visibility + | ++ version 1 + | +(background - core) | +(static HELM directory) | ++ version 1 + | ++ library + | +(static LDDL directory) | +
Contents of the Specification ![[butterfly]](http://lambdadelta.info/images/b4.png "\lambda\delta butterfly")
+
+
+ This specification comprises a collection of checked
applications of λδ version 2.
- In particular it contains the components below.
+ In particular it contains the components below.
- - MLTT1. - Martin-Löf's Type Theory with one universe - using λδ as theory of expressions. -
- Functional. - The validation algorithm for λδ as implemented in - Helena 0.8. -
Summary of the Specification
- Here is a numerical acount of the specification's contents
+
-
-
+
- + MLTT1. + Martin-Löf's Type Theory with one universe + using λδ as theory of expressions. + +
-
+
- + Functional. + The validation algorithm for λδ as implemented in + Helena 0.8. + +
-
+
- + Examples. + Terms of λδ with special features. + +
Summary of the Specification
+
+
+ Here is a numerical account of the specification's contents
and its timeline.
- | category | objects | |||||
| sizes | files | 5 | characters | 5613 | nodes | 10024 |
| propositions | theorems | 4 | lemmas | 1 | total | 5 |
| concepts | declared | 3 | defined | 10 | total | 13 |
- 2012 February 24.
+ ++
+ +
++ +category +units ++ +
++ +
++ +
++ +
++ +
++ +sizes +characters (files) +377 (1) +nodes (objects) +779 (6) +intrinsic loss factor +2.1 ++ +propositions +theorems +2 +lemmas +1 +total +3 ++ + +concepts +declared +0 +defined +3 +total +3 +-
+
- + 2017 March 6. + The Examples component is moved from the Core directory. + +
-
+
- + 2012 February 24. The Applications directory is started. -
- 2011 December 20. + +
-
+
- + 2011 December 20. The Functional component is started - inside the specification of λδ version 2. -
- 2011 December 12. + inside the specification of λδ version 2. + +
-
+
- + 2011 December 12. The MLTT1 component is started. -
Logical Structure of the Specification-The source files are grouped in planes and components - according to the following table. - Each component contains its own notation file. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). + + +Logical Structure of the Specification+
+ This table reports the specification's components and their planes.-- -component plane files MLTT1 genv_primitive judgement functional reduction and type machine rtm rtm_step ( ? ⨠? ) unfold lift ( â[?,?] ? ) subst ( [?â?] ? ) Physical Structure of the Specification-The source files are grouped in directories, - one for each component. --![[Generated from XML via XSL]](http://lambdadelta.info/images/xml_xsl2.png "Generated from XML via XSL")
![[PNG used here]](http://lambdadelta.info/images/PNGnow2.png "PNG used here")
![[Viewable with any browser]](http://www.anybrowser.org/campaign/bvgraphics/abtfile.png "Viewable with any browser")
Last update: 2013-02-18T20:41:26+01:00- ++++ +
++ +component +plane +files ++ + +examples +terms with special features +ex_cpr_omega +++
+ ++ +
+++
+Last update: Fri, 24 Nov 2017 21:00:01 +0100+