SEQUBE: Sequent calculus for programming languages

The duality of construction

Paul Downen and Zena M. Ariola. (2014). European Symposium on Programming, Grenoble, France (ESOP2014).
We explore the duality of construction and deconstruction in the presence of different evaluation strategies. We characterize an evaluation strategy by the notion of substitutability, given by defining what is a value and a co-value, and we present an equational theory that takes the strategy as a parameter. The theory may be extended with new logical connectives, in the form of user-defined data and co-data types, which are duals of one another. Finally, we explore a calculus with composite evaluation strategies that allow for more flexibility over evaluation order by mingling multiple primitive strategies within a single program.


Structures for structural recursion

Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. (2015). International Conference on Functional Programming, Vancouver, BC, Canada (ICFP2015).
Our goal is to develop co-induction from our understanding of induction, putting them on level ground as equal partners for reasoning about programs. We investigate several structures which represent well-founded forms of recursion in programs. These simple structures encapsulate reasoning by primitive and noetherian induction principles, and can be composed together to form complex recursion schemes for programs operating over a wide class of data and co-data types. At its heart, this study is guided by duality: each structure for recursion has a dual form, giving perfectly symmetric pairs of equal and opposite data and co-data types for representing recursion in programs. Duality is brought out through a framework presented in sequent style, which inherently includes control effects that are interpreted logically as classical reasoning principles. To accommodate the presence of effects, we give a calculus parameterized by a notion of strategy, which is strongly normalizing for a wide range of strategies. We also present a more traditional calculus for representing effect-free functional programs, but at the cost of losing some of the founding dualities.


Sequent calculus as a compiler intermediate language

Paul Downen, Luke Maurer, Zena Ariola, and Simon Peyton Jones. (2016). International Conference on Functional Programming, Nara, Japan (ICFP2016).
The λ-calculus is popular as an intermediate language for practical compilers. But in the world of logic it has a lesser-known twin, born at the same time, called the sequent calculus. Perhaps that would make for a good intermediate language, too? To explore this question we designed Sequent Core, a practically-oriented core calculus based on the sequent calculus, and used it to re-implement a substantial chunk of the Glasgow Haskell Compiler.