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

Lead Research Organisation: Heriot-Watt University
Department Name: S of Mathematical and Computer Sciences

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.

Publications

10 25 50

Related Projects

Project Reference Relationship Related To Start End Award Value
EP/K031864/1 01/09/2013 29/02/2016 £280,590
EP/K031864/2 Transfer EP/K031864/1 01/03/2016 31/01/2017 £65,323
 
Description The grant investigated new algorithms allowing to automatically prove and/or check certain properties of software, such as safety and security.
These algorithms are used in programming languages via types or via static analysis.

We developed a range of algorithms, ranging from Coalgebraic logic programming to Proof relevant corecursive resolution and non-termination checkers that introduced novel solutions to a range of existing problems in programming language design.
In particular, we embedded these algorithms into type class inference in a programming language Haskell and vi abstract compilation -- into a programming language Java.
Exploitation Route The finding may be integrtaed in a range of programming languages. This project proved the concept by using them in Haskell and Java.
Sectors Digital/Communication/Information Technologies (including Software)

URL http://www.macs.hw.ac.uk/~ek19/CoALP/
 
Description The research discussions are on the way of 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.
First Year Of Impact 2016
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 09/2020 
End 08/2023
 
Description Continuous Verification of Neural Networks
Amount £90,848 (GBP)
Organisation Defence Science & Technology Laboratory (DSTL) 
Sector Public
Country United Kingdom
Start 04/2020 
End 03/2021
 
Description SICSA PEER grant
Amount £2,500 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 09/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 09/2017 
End 09/2017
 
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 Machine-Learning for theorem Proving in Haskell 
Organisation Bangladesh University of Engineering and Technology
Department Department of Computer Science and Engineering
Country India 
Sector Academic/University 
PI Contribution Research discussions, paper and grant writing with Moa Johansson
Collaborator Contribution Research discussions, paper and grant writing
Impact Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson, Ewen Maclean: Proof-Pattern Recognition and Lemma Discovery in ACL2. LPAR 2013: 389-406
Start Year 2013
 
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 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 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 Coalgebra, Horn Clause Logic Programming and Types, 28-29 November 2016, Edinburgh, 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 International workshop disseminating the grant findings. Attracted participants from major UK universities, industries (Microsoft, Google); as well as research students.
Year(s) Of Engagement Activity 2017
URL https://ff32.host.cs.st-andrews.ac.uk/coalpty16/