Type systems are a powerful tool in modern programming languages. We argue that, to be successfully adopted by the logic programming community, the first step is to design a type system that is able to catch obvious and relevant errors at compile-time. To do so, we defined a new type […]
Type theory
2 posts
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)