![[lambdadelta home]](http://lambdadelta.info/images/crux_32.png "lambdadelta home")
+
+
+
+ +
+
+
+
+
+ | + 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.
- -
+
- - MLTT1. - Martin-Löf's Type Theory with one universe - using λδ as theory of expressions. + 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. + Functional. + The validation algorithm for λδ as implemented in + Helena 0.8.
- + Examples. + Terms of λδ with special features. + +
- - 2012 February 24. + 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. + 2011 December 12. The MLTT1 component is started.
-
+
Summary of the Specification
- Here is a numerical acount of the specification's contents
+
-
+
Summary of the Specification
+
+
+ Here is a numerical account of the specification's contents
and its timeline.
- Nodes are counted according to the "intrinsinc complexity measure"
- [F. Guidi: "Procedural Representation of CIC Proof Terms"
- Journal of Automated Reasoning 44(1-2), Springer (February 2010),
- pp. 53-78].
-
+
-
| category | -objects | -+ | category | +units | +
|
- + |
|
- + |
|
- + |
|
- + |
|
| sizes | -files | -4 | -characters | -2567 | -nodes | -3637 | +sizes | +characters (files) | +377 (1) | +nodes (objects) | +779 (6) | +intrinsic loss factor | +2.1 |
| propositions | -theorems | -2 | -lemmas | -1 | -total | -3 | +propositions | +theorems | +2 | +lemmas | +1 | +total | +3 |
| concepts | -declared | -3 | -defined | -9 | -total | -12 | +concepts | +declared | +0 | +defined | +3 | +total | +3 |
-
+
-
+
-
+
-
+
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 | -
- - |
- |||
| functional | -reduction and type machine | -rtm | -rtm_step ( ? ⨠? ) | +component | +plane | +files |
|
- - |
- relocation | -lift ( â[?,?] ? ) | -
- - |
+ examples | +terms with special features | +ex_cpr_omega |
Physical Structure of the Specification
- The source files are grouped in directories,
- one for each component.
-
-
- ![[Spacer]](http://lambdadelta.info/images/rainbow.png "lambdadelta rainbow rule")
+
@@ -191,6 +256,6 @@
-
+
+
@@ -191,6 +256,6 @@
Last update: Sun, 20 Jul 2014 16:13:31 +0200
-
+ Last update: Fri, 24 Nov 2017 21:00:01 +0100
+