Here is a numerical acount of the specification's contents
and its timeline.
@@ -51,117 +121,102 @@
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 |
+
|
- MLTT1 |
- |
- genv_primitive |
- judgement |
+ functional |
+ reduction and type machine |
+ rtm |
+ rtm_step ( ? ⨠? ) |
- functional |
- reduction and type machine |
- rtm |
- rtm_step ( ? ⨠? ) |
-
-
-
+ |
|
- unfold |
- lift ( â[?,?] ? ) |
- subst ( [?â?] ? ) |
-
-
- examples |
- |
- |
-
+ | relocation |
+ lift ( â[?,?] ? ) |
+
|
@@ -169,10 +224,6 @@
-
Physical Structure of the Specification
-
The source files are grouped in directories,
- one for each component.
-
@@ -199,6 +250,6 @@
-
Last update: Fri, 10 May 2013 18:19:21 +0200
+
Last update: Tue, 04 Nov 2014 16:28:52 +0100