Proper universe hierarchy

jonsterling / TT-Reflection

An experimental type theory with scoped equality reflection, and non-arbitrary proof search. This is basically a pared down version of Andromeda/Brazil, but with untyped reduction and a more Nuprl-like feel. Computational content of proofs is got via a realizability-based extraction. (Note: substitution is unsafe here, not because of a problem with the theory, but because I didn't understand how Bound works sadly.)

12 stars 0 forks source link

Proper universe hierarchy #14

Open jonsterling opened 10 years ago

jonsterling commented 10 years ago

Currently we are susceptible to Girard's paradox. This might be a good opportunity to learn how to replicate Sozeau's work on fixing Coq.

ghost commented 10 years ago

"Hard" might be an understatement for this one :)

I'm interested in trying to understand what exactly he's done though if you have pointers to literature. Collecting some of the relevant material on wiki page would be a good start. Is it based on earlier work from Harper and Pollack?

ghost commented 10 years ago

I added some material to the wiki at Universes.

jonsterling commented 10 years ago

Thank you! I don't think the inconsistency is an emergency, but it will be good to learn the state of the art with the aim of implementing it at some point.