Skip Navigation

CIS PhD Student Downen wins Dissertation Fellowship

alt text

Ph.D. student Paul Downen has been awarded a UO College of Arts and Sciences Dissertation Research Fellowship, which will fully fund his tuition for the 2016-2017 academic year. The award is highly competitive and recognizes Downen's significant and original contribution to his discipline.

Downen's research expands a relatively new "proofs as programs" approach in which programming and proving properties are seen not just as complementary activities, but as the very same activity. It is known that there is a duality between logic and computation. It is difficult, though, to find an adequate, clear and useful expression in logic of several programming language features that are important in practice. Together with his research advisor Zena Ariola, Downen proposed using the sequent calculus in place of the better known system of natural deduction as a logical framework. Downen has shown how sequent calculus can be used as a lower level representation corresponding to the intermediate language of a programming language translator, providing a basis for reasoning about optimizing transformations and, in particular, for reasoning about side effects in programming.

In addition to working out the theoretical basis for sequent calculus as an intermediate representation in program translation, Downen is collaborating with a team of leading international researchers to assess the impact of sequent calculus in a widely used translator for the functional programming language Haskell. The Glasgow Haskell Compliler was chosen as a subject because Haskell is an advanced programming language that makes particularly heavy demands on transformation of the intermediate representation to produce machine code that efficiently exploits modern parallel computers.

Downen's work has appeared in the top publication venues in his field, and is already widely recognized in the international research community as a leading expert on delimited control in programming languages.