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

Currently, the project investigates:

**...whether Structural resolution can make Automated Theorem Proving better:**-
**More Structural** -
**More Constructive:** -
**... whether structural resolution can enrich programming language design via new Type Inference algorithms.**P.Fu, E.Komendantskaya, T.Schrijvers, A.Pond. Proof Relevant Corecursive Resolution Accepted to FLOPS'2016, Japan, 3-6 March 2016.

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 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. Johann, E. Komendantskaya and V.Komendantskaya. Structural Resolution for Logic Programming. Technical Communications of ICLP 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.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.

P.Fu and E.Komendantskaya. A Type Theoretic Approach to Structural Resolution. Pre-proceedings of LOPSTR 2015.

**And whether this will bring more precise methods of operational semantics to automated proof search, leading to richer coinductive algorithms.**

- Katya Komendantskaya, University of Dundee, PI
- John Power, University of Bath, co-PI
- Peng Fu, University of Dundee, RA
- Frantisek Farka, PhD student
- Jonathan Heras, University of Rioja, former RA
- Martin Schmidt, University of Osnabrueck, visiting PhD student
- Vladimir Komendantsky, Moixa UK , London, former RA
- Andrew Pond, University of Dundee, internship student

- 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

Structural resolution: three-tier calculus for proofs in first-order Horn logic programming, semi-decision for productivity of logic programs via guardednes checks.

- Structural resolution: Productivity Checker and Coinductive Proof Inference implementation in Haskell, by Frantisek Farka. (2015)
- Structural resolution and Productivity Checker implementationin parallel Go , by Martin Schmidt. (2015)
- Haskell implementation. 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)
- 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. Project's webpage.
- P.Fu, E.Komendantskaya, T.Schrijvers, A.Pond. Proof Relevant Corecursive Resolution Accepted to FLOPS'2016, Japan, 3-6 March 2016. Project's webpage.
- 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, John Power and Martin Schmidt. Coalgebraic Logic Programming: from Semantics to Implementation. 39 pages. Journal of Logic and Computation, 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.
- 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 Parallélisme (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 katya ** at** computing.dundee.ac.uk