Ekaterina Komendanskaya
(University of Dundee)
Untyped Recursion and Corecursion in Logic Programming: Computational and Semantic Perspective

This talk will consist of two parts. Part 1 will be a general survey of recursive and corecursive methods in logic programming. I will start with a broad picture of the most important results concerning declarative (Herbrand model) semantics for logic programs with recursion and corecursion and then discuss their relation to the operational semantics of logic programming. Coalgebraic Logic Programming (CoALP) [Komendantskaya & Power, 2010-2014] arose from category-theoretic study of operational semantics of PROLOG and has now become a stand-alone programming language in its own right. Semantically, it unifies several existing approaches to recursion and corecursion in logic programming. Computationally, it extends the existing algorithms of automated proof search with corecursion and parallelism. In Part 2 of my talk, I will show how CoALP allowed, for the first time, to formulate a coherent theory of termination and productivity of untyped corecursion in logic programming, matching the theory of termination and productivity in Typeful Functional Languages.