Graph of dependencies generated by Dependtohtml

Since the development is parametric, the parameters are defined in the main file, which glues together all the others, using Load. Theory of PTS with abstract subtyping:

- Definition of terms and substitution
- Environments
- Abstract subtyping rule
- Abstract PTS structure
- Metatheory of PTS
- Type-checking algorithms

- Reduction operators
- Normal forms and head normal forms
- Conversion algorithm
- Subject Reduction property w.r.t the reduction operators

- Cumulative PTS structure
- Definition of cumulativity
- Decidability of cumulativity
- Type-checking cumulative PTS

- Definition of beta and delta reductions
- Subject Reduction for beta and delta
- Definition of confluence and the Tait-Martin-Lof proof
- Confluence of beta-delta-reduction
- Confluence of beta-reduction alone

Examples of sort inclusion:

- Type of sorts for both V5.10 and V6.2,
- Sorts of Coq V5.10,
- Sorts of Coq V6.2,
- Type-checker for Coq V5.10, extraction command
- Type-checker for Coq V6.2, extraction command
- Type-checker for Coq V6.2 (no delta), extraction command
- Extracted program

Library files:

Coq files compiled on: Dec 23 1998 15:55:19

The Coq Proof Assistant, version V6.2.3 - Type not extracted (December 1998)

compiled on Dec 18 1998 20:29:23