We give a constructive semantic proof of cut elimination for an intuitionistic formulation of Church’s Theory of Types (ICTT) extended with certain classes of axioms.

The argument uses a new technique extending ideas of Schütte, Takahashi, Andrews and Mahara. We introduce a new semantic criterion for cut-elimination extending prior work using the Nerode-Shore formulation of tableau proofs.

To the authors’ knowledge it is the first constructive semantic proof of cut elimination for ICTT and the extensions considered. We conclude with a discussion of higher-order logic programming with constraints. This is joint work with Olivier Hermant of MINES-ParisTech.