Coalgebraic Logic Programming, Structural Resolution, Type Class Resolution

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.

A Brief Description

This research project arose from our studies of coalgebraic semantics for logic programming and SLD-resolution proposed in research papers on Coalgebraic Logic Programming (CoALP) cf. [Komendantskaya and Power, 2011] below.

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.

See also:

Past and Present Project members:

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

Project partners:

  1. Davide Ancona, Genova University
  2. Tarmo Uustalu, Tallinn University of Technology
  3. Kevin Hammond, University of St Andrews
  4. Neil Ghani,University of Strathclyde
  5. Gopal Gupta, University of Texas at Dallas

Project Software and Prototype Implementations


CoALP and Structural Resolution full bibliography:

  1. 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.
  2. E.Komendantskaya and J.Power. Logic programming: laxness and saturation. Submitted to Journal of Logic and Algebraic Methods in Programming. 30 pages, 2016.
  3. F.Farka, E.Komendantskaya, K.Hammond and P.Fu. Coinductive Soundness of Corecursive Type Class Resolution. Pre-proceedings of LOPSTR'16, Edinburgh, UK.
  4. E.Komendantskaya, P.Johann and M.Schmidt. A Productivity Checker for Logic Programming. Pre-proceedings of LOPSTR'16, Edinburgh, UK.
  5. P.Fu and E.Komendantskaya. Operational Semantics of Resolution and Productivity in Horn Clause Logic. Journal ``Formal Aspect of Computing", 22 pages, 2017.
  6. E.Komendantskaya and J.Power. Category theoretic semantics for theorem proving in logic programming: embracing the laxness. Coalgebaric methods in Computer Sceince (CMCS'16).
  7. 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.
  8. 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.
  9. P.Fu, E.Komendantskaya, T.Schrijvers, A.Pond. Proof Relevant Corecursive Resolution Accepted to FLOPS'2016, Japan, 3-6 March 2016.
  10. P.Fu and E.Komendantskaya. A Type Theoretic Approach to Resolution. LNCS post-proceedings of LOPSTR 2015.
  11. 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.
  12. P. Johann, E. Komendantskaya and V.Komendantskiy. Structural Resolution for Logic Programming. Technical Communications of ICLP 2015.
  13. P.Fu and E.Komendantskaya. A Type Theoretic Approach to Structural Resolution. Pre-proceedings of LOPSTR 2015.
  14. 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.
  15. E.Komendantskaya, M.Schmidt and J.Heras. Exploiting Parallelism in Coalgebraic Logic Programming. Electr. Notes Theor. Comput. Sci. 303: 121-148 (2014).
  16. 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.
  17. E.Komendantskaya and J.Power. Coalgebraic derivations in logic programming. International conference Computer Science Logic, CSL'11. LIPICS proceedings.
  18. 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.
  19. 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.
  20. 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.

CoALP and Structural Resolution talks and presentations:

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

Contact

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