### Equality is typable in any Pure Type Systems (Based on a paper to
appear)

**Abstract:**

Pure Type Systems are usually described in two different ways, one that
uses an external notion of computation like beta-reduction,

and one that
relies
on a typed judgment of equality, directly in the typing system.

For a long time, the question to know whether both presentations described the
same theory. A first step toward this equivalence has

been made by Adams for a
particular class of PTS called functional. Then, his result
has been relaxed to all semi-full PTS in previous work.

In this paper, we finally give a positive answer to the general issue, and
prove that
equivalence holds for any Pure Type System.

Read Me

html coqdoc

tar file: Tested with the
trunk version of Coq and v8.3.
Please modify the Makefile to point out where coqc is located.

Helper file to link my phd dissertation to
the .v files.

A dependency graph of the modules involved.

Back to main page.

* Last modified Nov 18 2010*