+
+
+ +
+
+
+
+
+ + 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
+
+ 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].
-
+
-
sizes | files | -4 | +1 | characters | -2567 | +217 | nodes | -3637 | +0 |
propositions | theorems | -2 | +0 | lemmas | -1 | +0 | total | -3 | +0 |
concepts | declared | -3 | +0 | defined | -9 | +0 | total | -12 | +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.
-
+
-
-
Physical Structure of the Specification
- The source files are grouped in directories,
- one for each component.
-
-
-
+
@@ -191,6 +258,6 @@
-
+
@@ -191,6 +258,6 @@
Last update: Thu, 09 Oct 2014 20:11:24 +0200
-
+ Last update: Sun, 22 Jan 2017 20:42:51 +0100
+