Reduction Free Normalisation for a proof irrelevant type of propositions

03/07/2021
by   Thierry Coquand, et al.
0

We show normalisation and decidability of convertibility for a type theory with a hierarchy of universes and a proof irrelevant type of propositions, close to the type system used in the proof assistant Lean. Contrary to previous arguments, the proof does not require explicitly to introduce a notion of neutral and normal forms.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset