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:
- 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
Project partners:
- 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
Project Software and Prototype Implementations
CoALP and Structural Resolution full bibliography:
- 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.
CoALP and Structural Resolution talks and presentations:
-
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.
Contact
Please address any queries about this project to ek19 at hw.ac.uk