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].

Filter by
Sorted by
Tagged with
11 votes
1 answer

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 ...
Trebor's user avatar
  • 3,688