Implementation of Dependent Types

I started to implement dependent types in 85, for checking Girard's Paradox, mainly by copying and adapting Gerard Huet's original implementation. One main issue was how to represent the notion of definitions. In 95, while working with Dan Synek on implementation of Half, I tried to follow a denotational approach. This is summarized in the following documents.

This approach has been summarized by Andras Kovacs "Dependent type checking involves execution of arbitrary functional programs at compile time. For executing functional programs, the standard practice (used in virtually all functional languages) is to have Immutable program code, which may be machine code or interpreted code. Runtime objects, consisting of constructors and closures. The basic idea is to use the above setup during elaboration, with some extensions."

But the first motivation for a denotational approach was for showing correctness of the implementation.

This approach seems to be connected to the work of Peter Hancock in the 70s (never published).

In 88/89, I was working on implementing inductive types and inductive families as presented in this work (I implemented there an exemple at the end about ordinals using an inductively defined family and commented on this use. The original argument (due to Stan Wainer) did not use inductive families. The following proof in cubicaltt is closer to the original argument.) These works motivated trying to use pattern matching notations in type theory. The denotational approach suggests strongly that there is an essential difference between non indexed inductive types and indexed inductive types. I am not sure yet what is a nice denotational way to implement indexed inductive types. Maybe the work in cubicaltt, implemented following this denotational approach, suggests some ways to attack this problem.