applications of \lambda\delta version 2

cic:/matita/lambdadelta/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. 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].

category	objects
sizes	files	4	characters	2567	nodes	3637
propositions	theorems	2	lemmas	1	total	3
concepts	declared	3	defined	9	total	12

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
functional	reduction and type machine	rtm	rtm_step ( ? ⇨ ? )
	relocation	lift ( ↑[?,?] ? )

Physical Structure of the Specification

The source files are grouped in directories, one for each component.

Last update: Sun, 20 Jul 2014 16:13:31 +0200