This page supports the EPSRC grant **Coalgebraic Logic Programming for Type Inference: parallelism and corecursion for a
new generation of programming languages**,
2013-2017. Joint with John Power,
University of Bath.

In the course of this project, CoALP helped us to discover a method of ``Structural Resolution" - a proof method for Horn Clause Logic that is hybrid between Term-rewriting and First-order resolution. This new kind of resolution allowed us to give a structural reformulation for proof-search algorithms in logic programming.

Towards the second half of the project, we have been working on type-theoretic semantics of logic programming and its applications to Type Class inference in Haskell; as well as refinements of categorical (coalgebraic) semantics of Horn Clause logic.

- Workshop on Coalgebra, Horn Clause Logic Programming and Types, 28-29 November 2016, Edinburgh, UK.
**Workshop on Type inference and Automated Proving, 12 May 2015, Dundee, UK.**

- Katya Komendantskaya, Heriot-Watt University, PI
- John Power, University of Bath, co-PI
- Peng Fu, RA in Dundee and Heriot-Watt 2013-2016
- Martin Schmidt, visiting PhD student in Dundee in 2013, RA at Heriot-Watt in 2016
- Frantisek Farka, PhD student, Heriot-Watt university and university of St Andrews, 2015-2017
- Yue Li, PhD student, Heriot-Watt University, 2016-2019
- Jonathan Heras, University of Rioja, former RA, in 2013
- Vladimir Komendantsky, Moixa UK , London, RA at Dundee in 2013
- Andrew Pond, internship student at Dundee in 2014, 2015

- Davide Ancona, Genova University
- Tarmo Uustalu, Tallinn University of Technology
- Kevin Hammond, University of St Andrews
- Neil Ghani,University of Strathclyde
- Gopal Gupta, University of Texas at Dallas

- Coalgebraic Logic Programming, Main page on GitHub, 2016. Martin Schmidt, Katya Komendantskaya, Yue Li.
- Structural resolution (three-tier calculus for proofs in first-order Horn logic programming): Productivity Checker and Coinductive Proof Inference implementation in Haskell, by Frantisek Farka. (2015)
- Structural resolution and Productivity Checker implementation in parallel Go , by Martin Schmidt. (2015)
- First Haskell implementation of CoALP. By Vladimir Komendantsky, Jonathan Heras, Andrew Pond. (2013-2015)
- Prototype-2: CoALP implemented in Parallel Go; used for studying parallelism. By Martin Schmidt. (2012-2014)
- Prototype-1: CoALP implemented in Prolog. By Martin Schmidt. (2011-2012)

**Older prototypes and experiments:**

- Luca Franceschini, Davide Ancona and Ekaterina Komendantskaya. Structural Resolution for Abstract Compilation of Object-Oriented Languages. Workshop on Coalgebra, Horn Clause Logic Programming and Types, 28-29 November, Edinburgh, full version appeared as MSc thesis of L.Franceschini, U.Genova, 2016.
- E.Komendantskaya and J.Power. Logic programming: laxness and saturation. Submitted to Journal of Logic and Algebraic Methods in Programming. 30 pages, 2016.
- F.Farka, E.Komendantskaya, K.Hammond and P.Fu. Coinductive Soundness of Corecursive Type Class Resolution. Pre-proceedings of LOPSTR'16, Edinburgh, UK.
- E.Komendantskaya, P.Johann and M.Schmidt. A Productivity Checker for Logic Programming. Pre-proceedings of LOPSTR'16, Edinburgh, UK.
- P.Fu and E.Komendantskaya. Operational Semantics of Resolution and Productivity in Horn Clause Logic. Journal ``Formal Aspect of Computing", 22 pages, 2017.
- E.Komendantskaya and J.Power. Category theoretic semantics for theorem proving in logic programming: embracing the laxness. Coalgebaric methods in Computer Sceince (CMCS'16).
- E.Komendantskaya, John Power and Martin Schmidt. Coalgebraic Logic Programming: from Semantics to Implementation. 39 pages. Journal of Logic and Computation 2016 26 (2): 745-78.
- E.Komendantskaya and P.Johann. Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic. Submitted to ACM Transcations in Computational Logic. 36 pages, November 2015.
- P.Fu, E.Komendantskaya, T.Schrijvers, A.Pond. Proof Relevant Corecursive Resolution Accepted to FLOPS'2016, Japan, 3-6 March 2016.
- P.Fu and E.Komendantskaya. A Type Theoretic Approach to Resolution. LNCS post-proceedings of LOPSTR 2015.
- E. Komendantskaya, P. Fu and P. Johann. Structural Resolution for Automated Verification, "Ideas paper"; 15th International Workshop on Automated Verification of Critical Systems AVOCS'15, Edinburgh.
- P. Johann, E. Komendantskaya and V.Komendantskiy. Structural Resolution for Logic Programming. Technical Communications of ICLP 2015.
- P.Fu and E.Komendantskaya. A Type Theoretic Approach to Structural Resolution. Pre-proceedings of LOPSTR 2015.
- J.Heras, E.Komendantskaya and M.Schmidt. (Co)recursion in Logic Programming: Lazy versus Eager. Technical Communications of International Conference on Logic Programming (ICLP'14). Benchmarks for this paper.
- E.Komendantskaya, M.Schmidt and J.Heras. Exploiting Parallelism in Coalgebraic Logic Programming. Electr. Notes Theor. Comput. Sci. 303: 121-148 (2014).
- E.Komendantskaya, J.Power and M.Schmidt. Coalgebraic Logic Programming: implicit versus explicit resource handling. Workshop on Coinductive Logic Programming at International Conference on Logic Programming ICLP'12, Budapest, September 2012.
- E.Komendantskaya and J.Power. Coalgebraic derivations in logic programming. International conference Computer Science Logic, CSL'11. LIPICS proceedings.
- E.Komendantskaya and J.Power. Coalgebraic semantics for derivations in logic programming. International conference on Algebra and Coalgebra CALCO'11. Springer LNCS 6859, pp. 268-282.
- E.Komendantskaya and J.Power. Coalgebraic proofs in logic programming. Proceedings of the 18th Workshop on Automated Reasoning, Dept of Computing Science, University of Glasgow (Tech Report), 2011.
- E. Komendantskaya, G. McCusker and J. Power. Coalgebraic semantics for parallel derivation strategies in logic programming. Proceedings of AMAST'2010 - 13th International Conference on Algebraic Methodology and Software Technology (AMAST2010), 23-25 June 2010, Manoir St-Castin Quebec, Canada.

- Certified Automated Theorem Proving for Type Inference. Invited talk at University of Cambridge, 20 May 2016.
- Certified Automated Theorem Proving for Type Inference. Invited talk at University of Edinburgh (DREAM seminar), 10 May 2016.
- Automated Theorem Proving for Type Inference, Constructively. Invited talk at University of Bath, 03 May 2016.
- Automated Theorem Proving for Type Inference, Constructively. Dagstuhl Seminar 16131 Language Based Verification Tools for Functional Programs, 28 March - 01 April 2016.
- K.Komendantskaya. Structural Resolution Meets Curry Howard. Invited talk at Universities of Oxford (23 October 2015) and Birmingham (06 November 2015).
- K.Komendantskaya A 7-minute introduction to Structural Resolution. ICLP 2015, September 2015.
- P.Fu. A Type Theoretic Approach to Structural Resolution. Logic-based Program Synthesis and Transformation (LOPSTR), July 2015.
- E.Komendantskaya. Structural Resolution and Type Inference. Workshop on Type Inference and Automated Proving, May 2015 2014.
- P.Fu. Non-termination in Type Class Inference Workshop on Type Inference and Automated Proving, May 2015.
- E.Komendantskaya. Structural Resolution. Algebra and Coalgebra meet Proof Theory, 7 May 2015 2014.
- P.Fu. Horn Formulas as Types for Structural Resolution. Scottish Theorem Proving Seminar, Heriot-Watt University, March 2015.
- E.Komendantskaya. Structural Automated Proving. School of Computer Science, Universities of Swansea and Bath (by on-line conferencing), 11 December 2014.
- E.Komendantskaya. Untyped recursion and corecursion in logic programming: computational and semantic perspective. Logic group in the School of Mathematics, Leeds University, 8 October 2014.
- E.Komendantskaya. Coalgebraic Logic Programming. ICLP'14. 21 July 2014.
- E.Komendantskaya. Coalgebraic logic programming: corecursion and parallelism for untyped automated proof-search. Laboratoire de l'Informatique du Parallelisme (LIP), ENS (Ecole Normale Superior de) Lyon, France, 2 July 2014.
- E.Komendantskaya. Can Coalgebraic Logic Programming be useful for "Communication-based Computation"?. Communication-based Computation (CoCo) event, May 2014.
- E.Komendantskaya. Designing a small programming language, coalgebraically Shonan'13, Coinduction for Computation Structures and Programming Languages, 5-9 October 2013.
- E.Komendantskaya. Coalgebraic Logic Programming for Type Inference, Mathematically Structured Programming group (Strathclyde) research-away day. 6 June 2013.
- E.Komendantskaya. Coalgebraic Logic Programming: implicit versus explicit resource handling. Workshop on Coinductive Logic Programming at ICLP'12, Budapest, September 2012.
- E.Komendantskaya. Coalgebraic Derivations in Logic Programming. International Conference Computer Science Logic CSL'11. September 2011.
- E.Komendantskaya. Coinductive Logic Programming for Type Inference. International Workshop TYPES'11. September 2011.
- E.Komendantskaya. Coalgebraic Semantics for Parallel Derivation Strategies in Logic Programming. Scottish Category Theory Seminar. University of Glasgow. 13 May 2011.
- E.Komendantskaya. Coalgebraic derivations in Logic Programming. Automated Reasoning Workshop. University of Glasgow. 11 April 2011.
- E.Komendantskaya. Coalgebraic semantics for parallel derivation strategies in logic programming. International Conference AMAST'2010, Quebec, 23-25 June 2010.

Please address any queries about this project to ek19 ** at** hw.ac.uk