Coalgebraic Logic Programming for Type Inference
Lead Research Organisation:
University of Bath
Department Name: Computer Science
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Organisations
People |
ORCID iD |
| Anthony Power (Principal Investigator) |
Publications
A.J.Power
(2014)
Preface
Kinoshita Y
(2014)
Category theoretic structure of setoids
in Theoretical Computer Science
Komendantskaya E
(2016)
Coalgebraic logic programming: from Semantics to Implementation
in Journal of Logic and Computation
Komendantskaya E
(2013)
Coalgebraic Logic Programming: from Semantics to Implementation
Komendantskaya E
(2016)
Logic programming: laxness and saturation
Komendantskaya E
(2016)
CoALP-Ty'16
Komendantskaya E
(2018)
Logic programming: Laxness and saturation
in Journal of Logical and Algebraic Methods in Programming
Komendantskaya E.
(2017)
Preface
in Electronic Proceedings in Theoretical Computer Science, EPTCS
| Description | I have worked holistically on this, with relevant research that was partially done before the grant began being completed, and with new research being commenced. That has involved the completion of a succession of papers together with editing a proceedings. The latter included one paper that was done during the grant period but written (necessarily) by the co-PI in Dundee (now moved to Heriot-Watt). Of its nature, it amounted to testing what computation can actually be done as a result of the abstract mathematics. The other papers in the proceedings surrounded that, a general investigation of the combination of algebra and coalgebra with its interactions with logic and computation: note that the grant is inherently about using coalgebra to model logic programming. The mathematical work of the grant, which is the part for which I am responsible, is inherently abstract, with a number of applications. So I investigated a somewhat different, but related application on my visits to Japan (funded by a Japanese university and now by Royal Society), where we used coalgebraic-style techniques to model "setoids", which form a kind of logic that underlies the programming language Agda, which is broadly a sophisticated kind of logic programming language, reflecting a kind of extension to logic programming as we said we would study. I also used the underlying category theoretic techniques, in collaboration with colleagues in Bath, to model game semantics. And we finished work on our first journal paper that was directly on the narrow topic of the grant, and commenced research on further work. The latter involved dealing with the key underlying mathematical problem, that of providing a precise category theoretic semantics for "coinductive trees" and variants. That has not been written up yet; nor have the details been checked; but it has begun very well. We have written another journal paper now that I think is particularly good, further refining the underlying mathematics and connecting our approach with that of a French/Italian group. Much of the writing for that was done on a Royal Society-funded visit to Australia, where I also spoke about the work. That is still in process, developing very well. We are currently extending the work to model recursion, which has long been a goal for us, since the Dundee group (now Heriot-Watt) developed coinductive trees and began detailed consideration of the different ways in which recursion appears. In the meantime, the Dundee group has continued its more applied work, which in turn is raising new mathematical questions, in particular in regard to modelling the various kinds of recursion that arise here. |
| Exploitation Route | I have given seminars on the work (upon invitation) at Cambridge, Oxford, Strathclyde, Edinburgh and Macquarie University in Australia over the past few years. several times in Cambridge and Edinburgh They were all received intelligently and well by substantial audiences. So I am optimistic that the mathematicians and theoretical computer scientists there will absorb the ideas into their own work. |
| Sectors | Digital/Communication/Information Technologies (including Software) Other |
| Description | Invited talk (Cambridge) |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Participants in your research and patient groups |
| Results and Impact | People had not noticed the issue I explained, and they asked a string of questions about it. It also led to email correspondence. In a somewhat circuitous way, it led to a proposal to apply for joint research involving Australia (one of the audience having recently done relevant joint work with a researcher based in Australia). |
| Year(s) Of Engagement Activity | 2015 |
| URL | http://www.talks.cam.ac.uk/talk/index/60903 |
| Description | Invited talk (YamCats) |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Regional |
| Primary Audience | Participants in your research and patient groups |
| Results and Impact | The talk led people to think about Logic Programming and Coalgebraic Logic Programming in a way that they had not previously done. They asked questions and clearly gave the approach some thought. YamCats is a Yorkshire and Midlands based seminar series on category theory. After my talk, I was invited to give a further talk at Cambridge. We also discussed the possibility of running a workshop arising from it. |
| Year(s) Of Engagement Activity | 2015 |
| URL | http://www2.le.ac.uk/departments/mathematics/extranet/staff-material/staff-profiles/simona-paoli/yor... |
| Description | Invited talk LFCS 30th anniversary |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | It was the 30th anniversary celebration workshop for the Laboratory for the Foundations of Computer Science at the University of Edinburgh. It was taped and made available to the wider world. |
| Year(s) Of Engagement Activity | 2016 |
| Description | Invited talks at Macquarie University |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Regional |
| Primary Audience | Professional Practitioners |
| Results and Impact | I was asked to give two talks at Macquarie University in Sydney, Australia: one to the Mathematics department as a whole; the other to specialists in my area. |
| Year(s) Of Engagement Activity | 2016 |
| Description | invited talk (ScotCats) |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Participants in your research and patient groups |
| Results and Impact | There was considerable discussion. It also helped me to refine my own thinking. It, along with the other talks and visits on the grant, has helped to progress a fundamentally new mathematical structure that I and assorted other leading researchers in the topic are confident will be of key importance. |
| Year(s) Of Engagement Activity | 2014 |
| URL | http://msp.cis.strath.ac.uk/fibs-2014/ |