+
+
+ +
+
+
+
+
+ + 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].
-
+
-
sizes | files | -4 | +1 | characters | -2567 | +377 | nodes | -3637 | +779 |
propositions | @@ -94,43 +176,45 @@|||||||||
concepts | declared | -3 | +0 | defined | -9 | +3 | total | -12 | +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.
-
+
-
-
functional | -reduction and type machine | -rtm | -rtm_step ( ? ⨠? ) | +functional | +reduction and type machine | +rtm | +rtm_step ( ? ⨠? ) |
+ |
|
- relocation | -lift ( â[?,?] ? ) | +relocation | +lift ( â[?,?] ? ) | +
+ + |
+ |
examples | +terms with special features | +ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta |
|
@@ -160,13 +252,8 @@
Physical Structure of the Specification
- The source files are grouped in directories,
- one for each component.
-
-
-
+
@@ -191,6 +278,6 @@
-
+
@@ -191,6 +278,6 @@
Last update: Tue, 30 Sep 2014 16:37:52 +0200
-
+ Last update: Sat, 01 Apr 2017 16:50:39 +0200
+