+
+
+ +
+
+
+
+
+ + 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.
- + 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 | +units |
|
@@ -74,99 +156,82 @@
||||||||||
sizes | -files | -5 | -characters | -4273 | -nodes | -4166 | +sizes | +characters (files) | +377 (1) | +nodes (objects) | +779 (6) | +intrinsic loss factor | +2.1 |
propositions | theorems | 2 | lemmas | -3 | +1 | total | -5 | +3 | |||||
concepts | -declared | -5 | -defined | -10 | -total | -15 | +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 ( ? ⨠? ) | +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.
-
-
-
+
@@ -191,6 +256,6 @@
-
+
@@ -191,6 +256,6 @@
Last update: Sun, 05 Oct 2014 16:38:32 +0200
-
+ Last update: Fri, 24 Nov 2017 21:00:01 +0100
+