Adding a top type and allowing non-normalizing terms

Published: Feb. 5, 2020, 1 a.m.

b'

Curry-style typing and realizability make it sensible to allow a top type to type every term, even non-normalizing ones.

'