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