Extensions of logic programming – Workshop on Trends, Extensions, Applications and Semantics of Logic Programming

Uli Sattler: Description Logics and Ontology Languages – an introduction and overview

hbasold — Thu, 14 May 2020 20:20:25 +0000

Attachments

TEASE-LP_Sattler (7 MB)

Dmitry Rozplokhas and Dmitry Boulytchev: Certified Semantics for Disequality Constraints

hbasold — Thu, 14 May 2020 12:50:17 +0000

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

Attachments

Abstract Dmitry Rozplokhas and Dmitry Boulytchev (127 kB)

Marco Maggesi and Enrico Tassi: Private types in Higher Order Logic Programming

hbasold — Thu, 14 May 2020 12:40:51 +0000

We report on ongoing work on introducing a mechanism for private types in a higher-order logic programming language such as λProlog.

Forum Full Abstract

Attachments

Abstract Marco Maggesi and Enrico Tassi (124 kB)

Dmitrii Kosarev and Dmitry Boulytchev: Relational Synthesis of Pattern Matching

hbasold — Thu, 14 May 2020 12:37:25 +0000

We present an approach to pattern matching code generation based on application of relational programming and, in particular, relational interpreters.

Forum Video Full Abstract

Attachments

Abstract Dmitrii Kosarev and Dmitry Boulytchev (130 kB)

Maria Kuklina and Ekaterina Verbitskaia: Supercompilation Strategies of Relational Programs

hbasold — Thu, 14 May 2020 12:31:08 +0000

In this paper we research methods of supercompilation in the context of relational program specialization. We implement a supercompiler for miniKanren with different unfolding strategies and compare them.

Forum Video Full Abstract

Attachments

Abstract Maria Kuklina and Ekaterina Verbitskaia (124 kB)

Ekaterina Verbitskaia, Irina Artemeva and Daniil Berezun: Binding-Time Analysis for miniKanren

hbasold — Thu, 14 May 2020 12:29:05 +0000

We present a binding-time analysis algorithm for miniKanren. It is capable to determine the order in which names within a program are bound and can be used to facilitate specialization and as a step of conversion into a functional language.

Forum Video Full Abstract

Attachments

Abstract Ekaterina Verbitskaia, Irina Artemeva and Daniil Berezun (49 kB)

Olivier Hermant and James Lipton: Eliminating Cuts in HoiC

hbasold — Thu, 14 May 2020 12:21:30 +0000

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

Attachments

Abstract Olivier Hermant and James Lipton (129 kB)