Archive for the 'Focusing' 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.

Focusing and higher-order abstract syntax

By Noam Zeilberger, from POPL 2008, available from Noam Zeilberger’s website:

Focusing is a proof-search strategy, originating in linear logic, that elegantly eliminates inessential nondeterminism, with one byproduct being a correspondence between focusing proofs and programs with explicit evaluation order. Higher-order abstract syntax (HOAS) is a technique for representing higher-order programming language constructs (e.g., ╬╗’s) by higher-order terms at the “meta-level”, thereby avoiding some of the bureaucratic headaches of first-order representations (e.g., capture-avoiding substitution).

This paper begins with a fresh, judgmental analysis of focusing for intuitionistic logic (with a full suite of propositional connectives), recasting the “derived rules” of focusing as iterated inductive definitions. This leads to a uniform presentation, allowing concise, modular proofs of the identity and cut principles. Then we show how this formulation of focusing induces, through the Curry-Howard isomorphism, a new kind of higher-order encoding of abstract syntax: functions are encoded by maps from patterns to expressions. Dually, values are encoded as patterns together with explicit substitutions. This gives us pattern-matching “for free”, and lets us reason about a rich type system with minimal syntactic overhead. We describe how to translate the language and proof of type safety almost directly into Coq using HOAS, and finally, show how the system’s modular design pays off in enabling a very simple extension with recursion and recursive types.

Associated Coq source files are here, and a list of erratum is here.