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

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).

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.