Archive for the 'Pronominal' Category

Focusing on binding and computation

By Daniel R. Licata, Noam Zeilberger and Robert Harper from LICS 2008, available from Robert Harper’s website:

Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both representing and computing with binding. This language is extracted as the Curry-Howard interpretation of a focused sequent calculus with two kinds of implication, of opposite polarity. The representational arrow extends systems of definitional reflection with the notion of a scoped inference rule, which permits the adequate representation of binding via higher-order abstract syntax. On the other hand, the usual computational arrow classifies recursive functions over such higher-order data. Unlike many previous approaches, both binding and computation can mix freely.

Following Zeilberger [POPL 2008], the computational function space admits a form of open-endedness, in that it is represented by an abstract map from patterns to expressions. As we demonstrate with Coq and Agda implementations, this has the important practical benefit that we can reuse the pattern coverage checking of these tools.

A universe of binding and computation

Daniel Licata and Robert Harper, from ICFP 2009, available from Harper’s website.

In this paper, we construct a logical framework supporting datatypes that mix binding and computation, implemented as a universe in the dependently typed programming language Agda 2. We represent binding pronominally, using well-scoped de Bruijn indices, so types can be used to reason about the scoping of variables. We equip our universe with datatype-generic implementations of weakening, substitution, exchange, contraction, and subordination-based strengthening, so that programmers are provided these operations for free for each language they define.

In our mixed, pronominal setting, weakening and substitution hold only under some conditions on types, but we show that these conditions can be discharged automatically in many cases. Finally, we program a variety of standard difficult test cases from the literature, such as normalization-by-evaluation for the untyped lambda-calculus, demonstrating that we can express detailed invariants about variable usage in a program’s type while still writing clean and clear code.

A video of Daniel Licata’s presentation at ICFP is available here.