Here is a numerical acount 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].
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 ( â[?,?] ? ) |
+
|
@@ -161,10 +224,6 @@
-
Physical Structure of the Specification
-
The source files are grouped in directories,
- one for each component.
-
@@ -191,6 +250,6 @@
-
Last update: Sat, 12 Oct 2013 19:38:34 +0200
+
Last update: Tue, 04 Nov 2014 16:28:52 +0100