COALGEBRAIC LOGIC PROGRAMMING FOR TYPE INFERENCE: Parallelism and Corecursion for New Generation of Programming Languages

Lead Research Organisation: University of Dundee
Department Name: Computing

Abstract

The main goal of typing is to prevent the occurrence of execution errors during the running of a program.
Milner formalised the idea, showing that ``well-typed programs cannot go wrong''. In practice, type structures provide a fundamental technique of reducing programmer errors. At their strongest, they cover most of the properties of interest to the verification community.

A major trend in the development of functional languages is improvement in expressiveness of the underlying type system, e.g., in terms of Dependent Types, Type Classes, Generalised Algebraic Types (GADTs), Dependent Type Classes and Canonical Structures. Milner-style decidable type inference does not always suffice for such extensions (e.g. the principal type may no longer exist), and deciding well-typedness sometimes requires computation additional to compile-time type inference.

Implementations of new type inference algorithms include a variety of first-order decision procedures, notably Unification and Logic Programming (LP), Constraint LP, LP embedded into interactive tactics (Coq's eauto), and LP supplemented by rewriting.

Recently, a strong claim has been made by Gonthier et al that, for richer type systems, LP-style type inference is more efficient and natural than traditional tactic-driven proof development.

A second major trend is parallelism: the absence of side-effects makes it easy to evaluate sub-expressions in parallel. Powerful abstraction mechanisms of function composition and higher-order functions play important roles in parallelisation. Three major parallel languages are Eden (explicit parallelism) Parallel ML (implicit parallelism) and Glasgow parallel Haskell (semi-explicit parallelism). Control parallelism in particular distinguishes functional languages.

Type inference and parallelism are rarely considered together in the literature. As type inference becomes more sophisticated and takes a bigger role in the overall program development, sequential type inference is bound to become a bottle-neck for language parallelisation.

Our new Coalgebraic Logic Programming (CoALP) offers both extra expressiveness (corecursion) and parallelism in one algorithm. We propose to use CoALP in place of LP tools currently used in type inference.

With the mentioned major developments in Corecursion, Parallelism, and Typeful (functional) programming it has become vital for these disjoint communities to combine their efforts: enriched type theories rely more and more on the new generation of LP languages; coalgebraic semantics has become influential in language design; and parallel dialects of languages have huge potential in applying common techniques across the FP/LP programming paradigm. This project is unique in bringing together local and international collaborators working in the three communities. The number of
supporters the project has speaks better than words about the timeliness of our agenda.


The project will impact on two streams of EPSRC's strategic plan: "Programming Languages and Compilers" and "Verification and Correctness". The project is novel in aspects of Theory (coalgebraic study of (co)recursive computations arising in automated proof-search); Practice (implementation of the new language CoALP and its embedding in type-inference tools); and Methodology (Mixed corecursion and parallelism).

Planned Impact

The proposed research lies in the intersection of the research fields Programming Languages and Compilers (via Parallel and Corecursive Programming) and Verification and Correctness (via Type Inference).
Both fields are identified by EPSRC for strategic growth (www.epsrc.ac.uk/ourportfolio/themes/ict/).

As CoALP is applied to type inference, this will have direct impact on both research and industrial applications of functional languages and theorem provers, and ultimately, wider areas of Software Security, Verification and Design. As our collaborator from Object-oriented programming community D. Ancona says, ``It is a general methodology that can be, at least in principle, fruitfully applied not only to type inference, but to several kinds of static analysis. ... it can be smoothly integrated with static analysis techniques developed for compiler technology".

Our proposed method will affect four areas beyond the academic community: Knowledge, Economy, Society and People. The project will have a long-term effect on Economy and Society, as it enhances technologies that ensure dependability and security of software. With demand for embedded computing in cars, smart phones, and other electronics, there has been increased interest in formal verification for software correctness. Alongside that, companies like Microsoft, Intel, Altran Praxis, QinetiQ, Siemens, BOSCH, Airbus, the Stanford Research Institute are keen players in a software verification Grand Challenge: an international effort for software correctness in industry. The pervasive nature of software means that software dependability plays a crucial role within the world economy and in security - from maintaining national security through to protecting personal data.

Our work aims to advance programming languages design, including logic programming, typed functional programming languages, and theorem provers. The proposed project will develop a pilot implementation of CoALP and will, within three years, provide a new interpreter (for logic programs) and a new compiler (for a functional language) ready to be taken by industries that currently use these languages, e.g. ABSInt, Erlang Solutions, Galois Inc., Parallel Scientific, Vector Fabrics, Alcatel-Lucent, Bank of America Merril Lynch, Barclays Capital Quantitative Analysis Group, Facebook, Google, Microsoft.

Already during its course, the project will have immediate effect on Knowledge and People. Recently, CS has seen major developments in Corecursion, Parallelism, and Typeful (functional) programming. It has become vital for these (disjoint) communities to combine their efforts: enriched type theories rely more and more on the new generation of LP languages; coalgebraic semantics has become influential in language design; and parallel dialects of languages have huge potential in applying common techniques across the FP/LP programming paradigm. This project is unique in bringing together local and international collaborators working in the three communities. The number of supporters the project has speaks better than words about the timeliness of our agenda. We will link the project outcomes with the listed Academic beneficiaries. Engagement with academics will form a critical part of the pathway towards economic and societal impact.
 
Description The grant's duration was 3 years.
In its first year, we studied the properties and extensions of coalgebraic logic programming. In particular:

- its parallel derivation algorithms;
- recursive and corecursive derivation algorithms;
- we formulated a more general opertaional semantics for untyped recursion and corecursion in first-order logic;
- we continued to implement CoALP

In its second year, we continued to work on above subjects, but also started to investigate a type-theoretic semantics of CoALP and other resolution-based automated theorem provers. This allowed us to apply findings of the first year in type class inference in Haskell.

In the third year, we focussed further on implementation and applications of the methods we developed in type inference.
Exploitation Route We see academic impact of this work in future applications of CoALP to type inference.

In particular, we published a research paper in FLOPS'16 showing how our methods can automate some difficult cases of type class inference in Haskell.

In the longer run, this research may affect industries that use Haskell or related provers (Idris, Agda) to program and/or verify software.
Sectors Digital/Communication/Information Technologies (including Software)

URL http://staff.computing.dundee.ac.uk/katya/CoALP/
 
Description The research discussions took place on how to embed our algorithms in Software produced by Claudio Russo, Microsoft Research. We applied our algorithms in Type class inference in Haskell, and we investigate how his work on type class inference in C# and F# can benefit from this. Research visit by C.Russo was hosted in November 2016. A visitor from JetBrains is hosted in 2019, to discuss applications of coinduction in relational programming.
Sector Digital/Communication/Information Technologies (including Software)
Impact Types Economic

 
Description AISEC: AI Secure and Explainable by Construction
Amount £2,200,000 (GBP)
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 08/2020 
End 08/2023
 
Description British Logic Colloquium Funding for Automated Reasoning Workshop, Dundee, April 2013
Amount £360 (GBP)
Funding ID http://www.computing.dundee.ac.uk/staff/katya/arw13/ 
Organisation British Logic Colloquium 
Sector Charity/Non Profit
Country United Kingdom
Start 03/2013 
End 04/2013
 
Description Carnegie Trust Research Internship
Amount £1,400 (GBP)
Organisation Carnegie Trust 
Sector Charity/Non Profit
Country United Kingdom
Start 05/2015 
End 08/2015
 
Description Continuous Verification of Neural Networks
Amount £90,848 (GBP)
Organisation Defence Science & Technology Laboratory (DSTL) 
Sector Public
Country United Kingdom
Start 03/2020 
End 03/2021
 
Description DTA PhD Studentship
Amount £70,000 (GBP)
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 09/2014 
End 04/2018
 
Description Practical Types
Amount £1,500 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 08/2013 
End 09/2014
 
Description SICSA Distinguished Visiting Fellow: P.Johann
Amount £1,400 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 07/2015 
End 08/2015
 
Description SICSA Industrial Proof of Concept grant Machine-Learning for Industrial Theorem Proving
Amount £10,000 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 08/2013 
End 04/2014
 
Description SICSA PEER grant
Amount £2,500 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 08/2016 
End 12/2016
 
Description SICSA PEER grant, 2017
Amount £395 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 08/2017 
End 09/2017
 
Description SICSA Workshop funding: Practical Types Summer School
Amount £6,750 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 06/2015 
End 07/2015
 
Description SICSA Workshop funding: Type Inference and Automated proving
Amount £300 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 04/2015 
End 05/2015
 
Description SICSA support for Automated Reasoning Workshop, Dundee, April 2013.
Amount £992 (GBP)
Funding ID http://www.computing.dundee.ac.uk/staff/katya/arw13/ 
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 03/2013 
End 04/2013
 
Description SICSA workshop funding: STP'15
Amount £400 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 09/2015 
End 10/2015
 
Description SecCon-NN: Neural Networks with Security Contracts - towards lightweight, modular security for neural networks
Amount £30,000 (GBP)
Organisation National Cyber Security Centre 
Sector Public
Country United Kingdom
Start 11/2019 
End 03/2020
 
Title COALP: coalgebraic logic programming interpreter 
Description An interpreter for a prover -- COALP -- that combined proof search and coinductive methods. 
Type Of Material Improvements to research infrastructure 
Year Produced 2016 
Provided To Others? Yes  
Impact Collaborations started. 
URL http://www.macs.hw.ac.uk/~ek19/CoALP/
 
Description Coalgebraic Logic Programming 
Organisation University of Bath
Department Department of Computer Science
Country United Kingdom 
Sector Academic/University 
PI Contribution Paper and grant writing, with John Power.
Collaborator Contribution Paper and grant writing.
Impact CMCS'16 research paper, journal paper in Journal of Logic and Computation
Start Year 2013
 
Description Coalgebraic Logic Programming for Object-Oriented programming languages 
Organisation University of Genoa
Department Department of Computer and Information Sciences
Country Italy 
Sector Academic/University 
PI Contribution Research Collaboration, paper writing with Davide Ancona
Collaborator Contribution Research Collaboration, paper writing
Impact We won an Erasmus grant to co-supervise an MSc student
Start Year 2014
 
Description Coalgebraic Logic Programming for Type Classes in Haskell 
Organisation University of Leuven
Department Department of Computer Science
Country Belgium 
Sector Academic/University 
PI Contribution Research Discussion, paper and grant writing with Tom Schrijvers
Collaborator Contribution Research Discussion, paper and grant writing
Impact Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, Andrew Pond: Proof Relevant Corecursive Resolution. FLOPS 2016: 126-143
Start Year 2014
 
Description Structural Resolution 
Organisation Appalachian State University
Department Department of Computer Science
Country United States 
Sector Academic/University 
PI Contribution Collaboration on the topic of Structural Resolution for Logic Programming: research, paper writing, grant writing
Collaborator Contribution ollaboration on the topic of Structural Resolution for Logic Programming: research, paper writing, grant writing
Impact One conference paper with P.Johann in ICLP'15, a journal paper with P.Johann (submitted), and a grant pro-proposal in preparation.
Start Year 2014
 
Title CoALP: Coalgebraic Logic programming in Haskell 
Description We present CoALP -- an implementation of Coalgebraic Logic programming. It is a dialect of first-order Horn-Clause logic that features lazy guarded corecursion and parallelism. CoALP arose from Coalgebraic semantics we developed in 2010-2012. The implementation was developed by the research team employed by the grant between 2013 and 2016. 
Type Of Technology Software 
Year Produced 2015 
Open Source License? Yes  
Impact This software was taken for further development by a new EPSRC grant Coalgebraic Logic Programming for Type Inference: parallelism and corecursion for a new generation of programming languages for parallelism and corecursion, 2013-2016. 
URL http://staff.computing.dundee.ac.uk/katya/coalp/
 
Title New Coalgebraic Logic Programming implementation 
Description New, advanced, implementation of CoALP interpreter, By E.Komendantskaya and M.Schmidt 
Type Of Technology Software 
Year Produced 2017 
Open Source License? Yes  
Impact The tool is applied in abstract compilation in Java, bu collaborators D.Ancona and L.Franceschini, Genova University, Italy 
URL http://www.macs.hw.ac.uk/~ek19/CoALP/
 
Title Nontermination checker in Haskell 
Description Non-termination checker for term rewriting written in Haskell by project's RA Peng Fu. 
Type Of Technology Software 
Year Produced 2016 
Open Source License? Yes  
Impact Research paper has been produced and is currently under review. 
URL https://github.com/Fermat/FCR
 
Description ALCOP Invited talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Structural Resolution and Universal Productivity. Invited talk at the 4th Workshop Algebra and Coalgebra meet
Proof Theory, Delft, 6-8 May 2015. About 30 people were present.
Year(s) Of Engagement Activity 2015
URL http://www.appliedlogictudelft.nl/alcop-2015/
 
Description BCS Panel 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Invited speaker at the Panel "Turing: Soluble and Insoluble" at the British Logic Colloquium, Edinburgh, September
2016. About 50 participants.
Year(s) Of Engagement Activity 2016
URL https://www.ed.ac.uk/informatics/news-events/stories/2016/british-logic-colloquium-2016
 
Description FLOC'18 invited talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Invited talk "Coalgebra and Automated Reasoning" at Coalgebra, Now! - a FLOC 2018 workshop, Oxford, UK, 8 July 2018.
Year(s) Of Engagement Activity 2018
URL https://www.coalg.org/coalgebra-now-floc18/
 
Description IFIP2.8 invited talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Coinduction in horn Clause Logic. Invited participant at IFIP Working Group 2.8 on Functional Programming,
Edinburgh, 11-16 June 2017.
Year(s) Of Engagement Activity 2017
 
Description Invited talk at ALCOP17. 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Horn Clause logic: the knowns and the unknowns. Invited talk at the 8th international workshop Algebra and
Coalgebra meets Proof Theory (ALCOP), Glasgow, 10-12 April 2017. About 50 people present.
Year(s) Of Engagement Activity 2017
URL https://personal.cis.strath.ac.uk/clemens.kupke/ALCOP2017/
 
Description Invited talk at Bath and Swansea 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Structural Automated Proving. Invited talk at School of Computer Science, Universities of Swansea and Bath (by on-line conferencing), 11 December 2014.
About 20 people participated.
Year(s) Of Engagement Activity 2014
 
Description Invited talk at Birmingham and Oxford 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Structural Resolution Meets Curry Howard. Invited talk at Birmingham University, 06 November 2015 and Oxford
University, 23 October 2015.
About 40 people participated.
Year(s) Of Engagement Activity 2015
 
Description Invited talk at Cambridge 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Certified Automated Theorem Proving for Type Inference. Invited talk at University of Cambridge, 20 May 2016,
and University of Edinburgh (DREAM seminar), 10 May 2016.
About 30 participants.
Year(s) Of Engagement Activity 2016
 
Description Invited talk at Dagstuhl and Bath 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Automated Theorem Proving for Type Inference, Constructively . Invited talk at Dagstuhl Seminar 16131 Language
Based Verification Tools for Functional Programs, 28 March - 01 April 2016. Invited talk at University of Bath, 03 May 2016.
About 60 participants across both talks.
Year(s) Of Engagement Activity 2016
URL https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=16131
 
Description Invited talk at Leeds 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Untyped recursion and corecursion in logic programming: computational and semantic perspective. Invited talk,
Logic group in the School of Mathematics, Leeds University, 8 October 2014.
About 20 people participated.
Year(s) Of Engagement Activity 2014
 
Description Invited talk at MGS 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Certified Automated Theorem Proving for Type Inference. Invited talk at Midlands Graduate School (MGS), Christmas meeting, Leicester, 13 December 2016. About 50 participants.
Year(s) Of Engagement Activity 2016
 
Description Invited talk at Shonan 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Designing a small programming language, coalgebraically. Invited talk at Shonan'13, "Coinduction for Computation Structures and Programming Languages", 5-9 October 2013.
The audience was ~ 50 people including a dozen PG students.
Year(s) Of Engagement Activity 2013
URL http://shonan.nii.ac.jp/shonan/blog/2012/11/17/coinduction-for-computation-structures-and-programmin...
 
Description Invited talk in Rostov 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Certified Theorem Proving for Type Inference Invited talk at the Conference "Programming Languages and Com-
pilers", Rostov, Russia, 3-5 April 2017. About 70 participants
Year(s) Of Engagement Activity 2017
URL http://plc.sfedu.ru/
 
Description Lyon talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Coalgebraic logic programming: corecursion and parallelism for untyped automated proof-search. Invited talk at
Laboratoire de l'Informatique du Parallelisme (LIP), ´ Ecole Normale Sup ´ erior de Lyon, France, 2 July 2014.
About a dozen people participated.
Year(s) Of Engagement Activity 2014
 
Description QMU invited talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Proof Carrying Plans - two invited talks at Queen Mary University (5 January 2019) and Birmingham University
(28 February 2019).
Year(s) Of Engagement Activity 2018
 
Description Shonan'17 invited talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Coinductive Uniform proofs. Invited talk at the Shonan meeting "Enhanced Coinduction", Shonan, Japan, 13-17
November 2017.
Year(s) Of Engagement Activity 2017
URL http://shonan.nii.ac.jp/shonan/blog/2016/09/07/4410/
 
Description Workshop on Type inference and Automated Proving, 12 May 2015, Dundee, UK. 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Workshop dedicated to discussions of Type inference in Programming languages, attracted ~ 50 participants, of which high proportion was postgraduate students
Year(s) Of Engagement Activity 2016
URL http://staff.computing.dundee.ac.uk/frantisekfarka/tiap/