[Agda] Research position "Coalgebraic Logic Programming for Type Inference"

[Ekaterina Komendantskaya]

We have a fixed-term position at the School of Computing, Dundee for a
postdoctoral researcher to work on the project

 Coalgebraic Logic Programming for Type Inference:

a new generation of languages for parallelism and corecursion.

 More details are available below and

at http://staff.computing.dundee.ac.uk/katya/CoALP/

For further inquiries please email me:

Katya Komendantskaya <katya at computing.dundee.ac.uk>



School of Computing

University of Dundee

Postdoctoral Researcher in

Coalgebraic Logic Programming for Type Inference

Fixed-term position for 2 years (extension possible).

Start date: between 1 July 2014 and 1 October 2014;

Salary scale: between £29,837 and £33,5562 per annum.

Closing Date for applications: 16 June 2014.


The School of Computing at the University of Dundee invites

applications for a postdoctoral researcher to work on an interdisciplinary
 project

 "Coalgebraic Logic Programming for type inference: a new generation of
languages  for parallelism and corecursion" (
http://staff.computing.dundee.ac.uk/katya/CoALP/).

 The project spans several subjects, among which are:

 -   -- Computational Logic,

-   -- (Coalgebraic) Operational semantics,

-   -- Functional Programming;

-   -- Logic Programming,

-   -- Recursion and Corecursion in Programming languages;

-- Category Theory,

-   -- Type Theory;

-   -- Compilers

-   -- Parallelism and Concurrency

 The project is jointly led by

Dr E.Komendantskaya, University of Dundee

and

Dr J.Power, University of Bath.


We are looking for a researcher to spend up to 29 months in the Dundee team
developing CoALP-based type inference.  This will involve close collaboration
with the existing group members, as well as interaction with the project
partners.  Research experience of at least a PhD level in computer science
or mathematics is essential, as is some knowledge of either functional
programming or  automated/interactive theorem provers.

  **************************************

 Project description:

 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.

 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 becomes more
sophisticated and takes a bigger role in the overall program development.

 In this project, we have devloped a new dialect of logic programming --
Coalgebraic Logic Programming (CoALP) that features both extra
expressiveness (via 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.

  See http://staff.computing.dundee.ac.uk/katya/CoALP/ for more details.


***************************************************************


Ekaterina Komendantskaya
Senior Lecturer, Head of PhD Studies
Room 1.04, Queen Mother Building

School of Computing, University of Dundee

Scotland, DD14HN

Tel: (+44) 01382384820
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140517/d6247e08/attachment-0001.html