We discuss the problem of cut elimination in an intuitionistic version of Church’s Type Theory with constraints, a problem that arises in considering executable fragments suitable for logic programming. Attachments Abstract Olivier Hermant and James Lipton (129 kB)