![[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 + | +
+ + |
+
| + citations + | ++ visibility + | ++ version 1 + | +(background - core) | +(static HELM directory) | ++ version 1 + | ++ library + | +(static LDDL directory) | +
Contents of the Specification ![[spacer]](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.
- - 2012 February 24. + 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 | +objects | +
|
- + |
|
- + |
|
- + |
|
- + |
|
| sizes | -files | -4 | -characters | -3926 | -nodes | -3637 | +sizes | +files | +1 | +characters | +217 | +nodes | +0 |
| propositions | -theorems | -2 | -lemmas | -1 | -total | -3 | +propositions | +theorems | +0 | +lemmas | +0 | +total | +0 |
| concepts | -declared | -3 | -defined | -9 | -total | -12 | +concepts | +declared | +0 | +defined | +0 | +total | +0 |
-
+
-
+
-
+
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 | -+ | component | +plane | +files | +
|
| functional | -reduction and type machine | -rtm | -rtm_step ( ? ⨠? ) | +functional | +reduction and type machine | +rtm | +rtm_step ( ? ⨠? ) |
| + |
|
- relocation | -lift ( â[?,?] ? ) | -+ | relocation | +lift ( â[?,?] ? ) | +
|
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 +258,6 @@
-
+
+
@@ -191,6 +258,6 @@
Last update: Tue, 11 Mar 2014 19:37:30 +0100
-
+ Last update: Sat, 16 Apr 2016 14:53:00 +0200
+