cic:/matita/lambda_delta/basic_2/ (λδ version 2)
System's Syntax and Behavior
This is a summary of the "block structure"
of the System's syntactic items and reductions.
* In terms only.
** In terms and local environments only.
*** In global environments only.
**** Sort level k in terms only.
Summary of the Specification
Here is a numerical acount of the specification's contents
and its timeline.
| category | objects |
|
|
|
|
|
| sizes | files | 113 | bytes | 422759 |
|
|
| propositions | theorems | 45 | lemmas | 450 | total | 495 |
| concepts | declared | 31 | defined | 39 | total | 70 |
- In progress.
Context-sensitive subject equivalence
for native type assignment.
- In progress.
Context-sensitive subject equivalence
for atomic arity assignment.
- 2012 March 15.
Context-sensitive strong normalization
for simply typed terms.
- 2012 January 27.
Support for abstract candidates of reducibility.
- 2011 September 21.
Confluence for context-sensitive parallel reduction.
- 2011 September 6.
Confluence for context-free parallel reduction.
- 2011 April 17.
Specification starts.
Logical Structure of the Specification
The source files are grouped in planes and components
according to the following table.
A notation file covering the whole specification is provided.
The notation for the relations or functions introduced in each file
is shown in parentheses.
Physical Structure of the Specification
The source files are grouped in directories,
one for each component.
Last update: 2012-03-15+01: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")