Questions tagged [extensional-type-theory]
Use for proof assistants or type theories featuring an equality type that has a reflection rule creating judgemental equalities out of them. See also [reflection].
1
question
11
votes
1
answer
244
views
Normalization by evaluation for extensional type theories
Is there material on how to implement normalization for (any flavor of) ETT?
This describes techniques related to doing untyped normalization. But there are (operational and semantic) problems when ...
- 3,688