De Bruijn notation as a nested datatype

By Richard Bird and Ross Paterson, in the Journal of Functional Programming, available from Ross Paterson’s website:

de Bruijn notation is a coding of lambda terms in which each occurrence of a bound variable x is replaced by a natural number, indicating the `distance’ from the occurrence to the abstraction that introduced x. One might suppose that in any datatype for representing de Bruijn terms, the distance restriction on numbers would have to maintained as an explicit datatype invariant. However, by using a nested (or non-regular) datatype, we can define a representation in which all terms are well-formed, so that the invariant is enforced automatically by the type system.

Programming with nested types is only a little more difficult than programming with regular types, provided we stick to well-established structuring techniques. These involve expressing inductively defined functions in terms of an appropriate fold function for the type, and using fusion laws to establish their properties. In particular, the definition of lambda abstraction and beta reduction is particularly simple, and the proof of their associated properties is entirely mechanical.

Associated Haskell files are here.

LNGen: Tool Support for Locally Nameless Representations

By Brian Aydemir and Stephanie Weirich, preprint, available from Brian Aydemir’s website:

Given the complexity of the metatheoretic reasoning about current programming languages and their type systems, techniques for mechanical formalization and checking of such metatheory have received
much recent attention. In previous work, we advocated a combination of locally nameless representation and cofinite quantification as a light- weight style for carrying out such formalizations in the Coq proof assistant. As part of the presentation of that methodology, we described a number of operations associated with variable binding and listed a number of properties, called “infrastructure lemmas”, about those operations that needed to be shown. The proofs of these infrastructure lemmas are straightforward but tedious.
In this work, we present LNgen, a prototype tool for automatically generating statements and proofs of infrastructure lemmas from Ott language specifications. Furthermore, the tool also generates a recursion scheme for defining functions over syntax, which was not available in our previous work. LNgen works in concert with Ott to effectively alleviate much of the tedium of working with locally nameless syntax. For the case of untyped lambda terms, we show that the combined output from the two tools is sound and complete, with LNgen automatically proving many of the key lemmas. We prove the soundness of our representation with respect to a fully concrete representation, and we argue that the representation is complete—that we generate the right set of lemmas—with respect to Gordon and Melham’s “Five Axioms of Alpha-Conversion.”

Associated Coq code can be found here.

Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables

By Murdoch J. Gabbay and Dominic P. Mulligan, from LFMTP 2009, available from Murdoch J. Gabbay’s website:

This paper develops the correspondence between equality reasoning with axioms using λ-terms syntax, and reasoning using nominal terms syntax. Both syntaxes involve name-abstraction: λ-terms represent functional abstraction; nominal terms represent atomsabstraction in nominal sets.

It is not evident how to relate the two syntaxes because their intended denotations are so different. We use universal algebra, the logic of equational reasoning, a logical foundation based on an equality judgement form which is spartan but which is sufficiently expressive to encode mathematics in theory and practice.

We investigate how syntax, algebraic theories, and derivability relate across λ-theories (algebra over λ-terms) and nominal algebra theories.

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 verified compiler for an impure functional language

By Adam Chlipala, from POPL 2010, available from Adam Chlipala’s website:

We present a verified compiler to an idealized assembly language from a small, untyped functional language with mutable references and exceptions. The compiler is programmed in the Coq proof assistant and has a proof of total correctness with respect to big-step operational semantics for the source and target languages. Compilation is staged and includes standard phases like translation to continuation-passing style and closure conversion, as well as a common subexpression elimination optimization. In this work, our focus has been on discovering and using techniques that make our proofs easy to engineer and maintain. While most programming language work with proof assistants uses very manual proof styles, all of our proofs are implemented as adaptive programs in Coq’s tactic language, making it possible to reuse proofs unchanged as new language features are added.

In this paper, we focus especially on phases of compilation that rearrange the structure of syntax with nested variable binders. That aspect has been a key challenge area in past compiler verification projects, with much more effort expended in the statement and proof of binder-related lemmas than is found in standard pencil and-paper proofs. We show how to exploit the representation technique of parametric higher-order abstract syntax to avoid the need to prove any of the usual lemmas about binder manipulation, often leading to proofs that are actually shorter than their pencil-and-paper analogues. Our strategy is based on a new approach to encoding operational semantics which delegates all concerns about substitution to the meta language, without using features incompatible with general-purpose type theories like Coq’s logic.

Program sources are available here (part of the LambdaTamer project), and a talk given at WMM 2009 is available here.

A previous posting of Adam Chlipala’s work on Parametric Higher Order Abstract Syntax can be found here.

Comparing operational models of name-passing process calculi

By Marcelo Fiore and Sam Staton, from CMCS 2004, available from Sam Staton’s website:

We study three operational models of name-passing process calculi: coalgebras on (pre)sheaves, indexed labelled transition systems, and history dependent automata. The coalgebraic model is considered both for presheaves over the category of finite sets and injections, and for its subcategory of atomic sheaves known as the Schanuel topos. We characterise the transition relations induced by the coalgebraic model, observing the differences between the first two models. Furthermore by imposing conditions on history dependent automata, this model is shown to become equivalent to the sheaf-theoretic coalgebraic model.

Revisiting cut-elimination: one difficult proof is really a proof

By Christian Urban and Bozhi Zhu, from RTA 2008, available from Christian Urban’s website:

Powerful proof techniques, such as logical relation arguments, have been developed for establishing the strong normalisation property of term-rewriting systems. The first author used such a logical relation argument to establish strong normalising for a cut-elimination procedure in classical logic. He presented a rather complicated, but informal, proof establishing this property. The difficulties in this proof arise from a quite subtle substitution operation, which implements proof transformation that permute cuts over other inference rules. We have formalised this proof in the theorem prover Isabelle/HOL using the Nominal Datatype Package, closely following the informal proof given by the first author in his PhD-thesis. In the process, we identified and resolved a gap in one central lemma and a number of smaller problems in others. We also needed to make one informal definition rigorous. We thus show that the original proof is indeed a proof and that present automated proving technology is adequate for formalising such difficult proofs.

Higher-order unification via explicit substitutions

By Gilles Dowek, Therese Hardin and Claude Kirchner, from Information and Computation, available from ScienceDirect:

Higher order unification is equational unification for βη-conversion. But it is not first order equational  unification, as substitution has to avoid capture. Thus, the methods for equational unification (such as narrowing) built upon grafting (i.e., substitution without renaming) cannot be used for higher order unification, which needs specific algorithms. Our goal in this paper is to reduce higher order unification to first order equational unification in a suitable theory. This is achieved by replacing substitution by grafting, but this replacement is not straightforward as it raises two major problems. First, some unification problems have solutions with grafting but no solution with substitution. Then equational unification algorithms rest upon the fact that grafting and reduction commute. But grafting and βη-reduction do not commute in λ-calculus and reducing an equation may change the set of its solutions. This difficulty comes from the interaction between the substitutions initiated by βη-reduction and the ones initiated by the unification process. Two kinds of variables are involved: those of βη-conversion and those of unification. So, we need to set up a calculus which distinguishes between these two kinds of variables and such that reduction and grafting commute. For this purpose, the application of a substitution of a reduction variable to a unification one must be delayed until this variable is instantiated. Such a separation and delay are provided by a calculus of explicit substitutions. Unification in such a calculus can be performed by well-known algorithms such as narrowing, but we present a specialised algorithm for greater efficiency. At last we show how to relate unification in λ-calculus and in a calculus with explicit substitutions. Thus, we come up with a new higher order unification algorithm which eliminates some burdens of the previous algorithms, in particular the functional handling of scopes. Huet’s algorithm can be seen as a specific strategy for our algorithm, since each of its steps can be decomposed into elementary ones, leading to a more atomic description of the unification process. Also, solved forms in λ-calculus can easily be computed from solved forms in λσ-calculus.

alphaKanren: A fresh name in nominal logic programming

By William E. Bird and Daniel P. Friedman, from WSFP 2007, available from William E. Bird’s website:

We present αKanren, an embedding of nominal logic programming in Scheme. αKanren is inspired by αProlog and MLSOS, and allows programmers to easily write interpreters, type inferencers, and other programs that must reason about scope and binding. αKanren subsumes the functionality, syntax, and implementation of miniKanren, itself an embedding of logic programming in Scheme. We present the complete implementation of αKanren, written in portable R 5 RS Scheme. In addition to the implementation, we provide introductions to miniKanren and αKanren, and several example programs, including a type inferencer for the simply typed λ-calculus.

Scheme source files can be found here.

Reasoning on an imperative object based calculus in higher-order abstract syntax

By Alberto Ciaffaglione, Luigi Liquori and Marino Miculan, from MERLIN 2003, available from Luigi Liquori’s website:

We illustrate the benefits of using Natural Deduction in combination with weak Higher-Order Abstract Syntax for formalizing an object-based calculus with objects, cloning, method-update, types with subtyping, and side-effects, in inductive type theories such as the Calculus of Inductive Constructions. This setting suggests a clean and compact formalization of the syntax and semantics of the calculus, with an efficient management of method closures. Using our formalization and the Theory of Contexts, we can prove formally the Subject Reduction Theorem in the proof assistant Coq, with a relatively small overhead.