The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

As far as I'm aware, this state of affairs just reflects the fact that since a type system is constructed inductively, certain types (notably -> and forall) must be defined quite early on.

I'm actually very interested in understanding what's involved in building up a simple type system (with universes) from scratch. If anyone's got any information on how to do this, I'd be glad to receive it. Thanks.

An inductive definition of a Martin-Löf style type system might look a bit complicated.

When trying to define it the "usual" way, the clause for dependent function (PI) types is problematic.

You can read more about it in page 49 (page 61 of the linked .ps file) of Stuart Allen's thesis

http://www.cs.cornell.edu/Info/Projects/NuPRL/documents/allen/NonTypeTheoreticSemantics.ps

He builds an "extensional" type system where types are denoted by partial equivalence relations (PERs) on terms, i.e. two terms 

are equal in a type iff they are related by its PER.

(Coq is "intensional" and its definition would look a bit different.)

We have formalized a similar construction in Coq :

http://www.nuprl.org/documents/Anand/TowardsAFormallyVerifiedProofAssistant.pdf

It also includes an alternate inductive-recursive definition in Agda, which is IMO more intuitive.

Regards,

-- Abhishek

http://www.cs.cornell.edu/~aa755/