Type theory – Workshop on Trends, Extensions, Applications and Semantics of Logic Programming https://www.coalg.org/tease-lp TEASE-LP, 28 and 29 May 2020, Virtual Event Wed, 27 May 2020 21:07:10 +0000 en-GB hourly 1 https://wordpress.org/?v=6.1.1 João Barbosa, Mário Florido and Vítor Santos Costa: Sound Type Assignment for Logic Programs https://www.coalg.org/tease-lp/2020/sound-type-assignment-for-logic-programs/ https://www.coalg.org/tease-lp/2020/sound-type-assignment-for-logic-programs/#respond Thu, 14 May 2020 12:30:10 +0000 https://www.coalg.org/tease-lp/?p=102 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 system which describes polymorphic well-typings for logic programs while respecting the main properties that make types useful and semantically sound. We now tackle the question of automatically producing a well typing for a logic program. We concentrated first on the implementation of a new type inference algorithm and its application to several logic programs.


Forum  Video Full Abstract

]]> https://www.coalg.org/tease-lp/2020/sound-type-assignment-for-logic-programs/feed/ 0 Olivier Hermant and James Lipton: Eliminating Cuts in HoiC https://www.coalg.org/tease-lp/2020/eliminating-cuts-in-hoic/ https://www.coalg.org/tease-lp/2020/eliminating-cuts-in-hoic/#respond Thu, 14 May 2020 12:21:30 +0000 https://www.coalg.org/tease-lp/?p=93 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.

Forum Full Abstract

]]> https://www.coalg.org/tease-lp/2020/eliminating-cuts-in-hoic/feed/ 0