Semantics – 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 Mon, 01 Jun 2020 17:24:18 +0000 en-GB hourly 1 https://wordpress.org/?v=6.1.1 Dmitry Rozplokhas and Dmitry Boulytchev: Certified Semantics for Disequality Constraints https://www.coalg.org/tease-lp/2020/certified-semantics-for-disequality-constraints/ https://www.coalg.org/tease-lp/2020/certified-semantics-for-disequality-constraints/#respond Thu, 14 May 2020 12:50:17 +0000 https://www.coalg.org/tease-lp/?p=119 We present an extension of our prior work on certified semantics for core miniKanren, introducing disequality constraints in the language. Semantics is parameterized by an exact definition of constraint stores, allowing us to cover different implementations. We extend our proof of search completeness to this language extension. The description and proofs are certified in Coq and a correct-by-construction interpreter is extracted.

Forum Full Abstract

]]> https://www.coalg.org/tease-lp/2020/certified-semantics-for-disequality-constraints/feed/ 0 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