<div dir="ltr"><div><span id="docs-internal-guid-d46f8874-0952-97b2-351b-777274ef00ad"><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">We have a fixed-term position at the School of Computing, Dundee for a postdoctoral researcher to work on the project </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;font-weight:bold;font-style:italic;vertical-align:baseline;white-space:pre-wrap">Coalgebraic Logic Programming for Type Inference: </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;font-weight:bold;font-style:italic;vertical-align:baseline;white-space:pre-wrap">a new generation of languages for parallelism and corecursion</span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">. </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">More details are available below and</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">at <a href="http://staff.computing.dundee.ac.uk/katya/CoALP/">http://staff.computing.dundee.ac.uk/katya/CoALP/</a></span></p>
<br><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">For further inquiries please email me:</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Katya Komendantskaya <</span><span style="font-size:16px;font-family:'Courier New';color:rgb(17,85,204);background-color:transparent;vertical-align:baseline;white-space:pre-wrap"><a href="mailto:katya@computing.dundee.ac.uk">katya@computing.dundee.ac.uk</a></span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">></span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<br>
<br><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:center"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">School of Computing</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:center"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">University of Dundee</span></p>
<br><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:center"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Postdoctoral Researcher in</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:center"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Coalgebraic Logic Programming for Type Inference</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:center"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Fixed-term position for 2 years (extension possible).</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:center"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Start date: between 1 July 2014 and 1 October 2014;</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:center"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Salary scale: between £29,837 and £33,5562 per annum. </span></p>
<br><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Closing Date for applications: 16 June 2014.</span></p>
<br><br><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">The School of Computing at the University of Dundee invites</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">applications for a postdoctoral researcher to work on an interdisciplinary project</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;font-weight:bold;font-style:italic;vertical-align:baseline;white-space:pre-wrap">"Coalgebraic Logic Programming for type inference: a new generation of languages for parallelism and corecursion" </span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">(</span><a href="http://staff.computing.dundee.ac.uk/katya/CoALP/" style="text-decoration:none"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;text-decoration:underline;vertical-align:baseline;white-space:pre-wrap">http://staff.computing.dundee.ac.uk/katya/CoALP/</span></a><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">).</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">The project spans several subjects, among which are: </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">-</span><span style="font-size:9px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> -- </span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Computational Logic, </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">-</span><span style="font-size:9px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> -- </span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">(Coalgebraic) Operational semantics,</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">-</span><span style="font-size:9px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> -- </span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Functional Programming; </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">-</span><span style="font-size:9px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> -- </span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Logic Programming,</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">-</span><span style="font-size:9px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> -- </span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Recursion and Corecursion in Programming languages;</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">-- Category Theory, </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">-</span><span style="font-size:9px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> -- </span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Type Theory;</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">-</span><span style="font-size:9px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> -- </span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Compilers</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">-</span><span style="font-size:9px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> -- </span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Parallelism and Concurrency</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">The project is jointly led by</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Dr E.Komendantskaya, University of Dundee</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">and</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">Dr J.Power, University of Bath.</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<br><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">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</span><span style="font-size:16px;font-family:Arial;background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">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.</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap">**************************************</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:16px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;text-decoration:underline;vertical-align:baseline;white-space:pre-wrap">Project description:</span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:'Times New Roman';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.3636363636363635;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:'Courier New';color:rgb(0,0,0);background-color:transparent;vertical-align:baseline;white-space:pre-wrap">The main goal of typing is to prevent the occurrence </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:'Courier New';color:rgb(0,0,0);background-color:transparent;vertical-align:baseline;white-space:pre-wrap">of execution errors during the running of a program.</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:Arial;background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.3636363636363635;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:'Courier New';color:rgb(0,0,0);background-color:transparent;vertical-align:baseline;white-space:pre-wrap">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.</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:'Courier New';color:rgb(0,0,0);background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:'Courier New';color:rgb(0,0,0);background-color:transparent;vertical-align:baseline;white-space:pre-wrap">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.</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:Arial;background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:'Courier New';color:rgb(0,0,0);background-color:transparent;vertical-align:baseline;white-space:pre-wrap">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.</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:'Courier New';color:rgb(0,0,0);background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:'Courier New';color:rgb(0,0,0);background-color:transparent;vertical-align:baseline;white-space:pre-wrap">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. </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:Arial;background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:Arial;background-color:transparent;vertical-align:baseline;white-space:pre-wrap"> </span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:'Courier New';color:rgb(0,0,0);background-color:transparent;vertical-align:baseline;white-space:pre-wrap">See </span><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"><a href="http://staff.computing.dundee.ac.uk/katya/CoALP/">http://staff.computing.dundee.ac.uk/katya/CoALP/</a> for more details.</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:'Courier New';background-color:transparent;vertical-align:baseline;white-space:pre-wrap"><br>
</span></p><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt;text-align:justify"><span style="font-size:16px;font-family:Arial;background-color:transparent;vertical-align:baseline;white-space:pre-wrap">***************************************************************</span></p>
<div><span style="font-size:16px;font-family:Arial;background-color:transparent;vertical-align:baseline;white-space:pre-wrap"><br></span></div></span></div><div><br></div><div>Ekaterina Komendantskaya <br>
</div><div><div><div>Senior Lecturer, Head of PhD Studies </div><div>Room 1.04, Queen Mother Building </div><div>School of Computing, University of Dundee </div>
<div>Scotland, DD14HN </div><div>Tel: (+44) 01382384820 </div><div>
<br></div><div><br></div><div><br></div></div></div>
</div>