cic:/matita/lambda_delta/apps_2/ (applications of λδ version 2)
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.
- Functional.
The validation algorithm for λδ as implemented in
Helena 0.8.
Summary of the Specification
Here is a numerical acount of the specification's contents
and its timeline.
| category | objects |
|
|
|
|
|
| sizes | files | 5 | bytes | 13143 |
|
|
| propositions | theorems | 4 | lemmas | 1 | total | 5 |
| concepts | declared | 3 | defined | 10 | total | 13 |
- 2012 February 24.
The Applications directory is started.
- 2011 December 20.
The Functional component is started
inside the specification of λδ version 2.
- 2011 December 12.
The MLTT1 component is started.
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).
| component | plane | files |
|
| MLTT1 | | genv_primitive | judgement |
| functional | reduction and type machine | rtm | rtm_step ( ? ⇨ ? ) |
| unfold | lift ( ↑[?,?] ? ) | subst ( [?←?] ? ) |
Physical Structure of the Specification
The source files are grouped in directories,
one for each component.
Last update: 2012-10-16T20:12:15+02:00
![[lambda_delta home]](http://lambda-delta.info/images/crux_32.png "lambda_delta home")
![[Spacer]](http://lambda-delta.info/images/rainbow.png "lambda_delta rainbow rule")
![[Generated from XML via XSL]](http://lambda-delta.info/images/xml_xsl2.png "Generated from XML via XSL")
![[PNG used here]](http://lambda-delta.info/images/PNGnow2.png "PNG used here")
![[Viewable with any browser]](http://www.anybrowser.org/campaign/bvgraphics/abtfile.png "Viewable with any browser")