Ulrich Berger

A realizability interpretation of Church's simple theory of types

2016 · Mathematical Structures in Computer Science

We give a realizability interpretation of an intuitionistic version of Church's Simple Theory of Types (CST) which can be viewed as a formalization of intuitionistic higher-order logic. Although definable in CST we include operators for …