Higher-Order and Symbolic Computation, 19(2/3)

The present issue is composed of journal versions of six papers from the second ACM SIGPLAN workshop MEchanized Reasoning about Languages with varIable and Names (MERLIN 2003), which was held in association with the federated meeting "Principles, Logics and Implementations of high-level programming languages" (PLI 2003, Uppsala, August 2003). A previous edition of the workshop was held in Siena, Italy, 2001, and a later edition was held in Tallinn, Estonia, 2005.

Currently, there is considerable interest in developing techniques and models for representing and reasoning formally about variables, names, binding structures, freshness predicates, higher-order abstract syntax, ... in programming languages. These techniques are of vital importance in applying computer-aided tools. Appropriate meta-languages and new programming languages, where the above notions are first-class citizens, have to be introduced. Recently, new meta-logical tools and methodologies have been proposed, such as inductive/coinductive definitions and associated schemata of recursion/corecursion, making programming and computer-aided formal reasoning on names and variables a reality.

The aim of the MERLIN workshops is to provide researchers and practitioners with a forum on state-of-the-art results and techniques in this field. Advances in these areas will have a significant impact on the programming language community at large, because they can lead to better and more robust methods for programming and for program reasoning.

The first two papers in this issue describe interesting case studies.

In "Mechanising lambda-calculus using a Classical First Order Theory of Terms with Permutations", Michael Norrish describes the mechanisation in HOL of some basic lambda-calculus theory. The difficulties arising from the use of the Barendregt Variable Convention are dealt with using Gordon and Melham's "five axioms of alpha-conversion".

In "Formal Compiler Construction in a Logical Framework", Jason Hickey and Aleksey Nogin face a typical situation where dealing correctly with variables and binders is fundamental: the design and implementation of a compiler. They present a new approach based on the use of higher-order abstract syntax and term rewriting in a Logical Framework, which guarantees the preservation of scoping, automating many frequently-occurring tasks including substitution and rewriting strategies.

The next four papers provide new insights in the theory of models of names, variables, and associated abstract structures.

"An Initial Algebra Approach to Term Rewriting Systems with Variable Binders" by Makoto Hamana, presents an extension of first-order term rewriting systems involving variable binding in the term language. This development follows the initial algebra approach in various functor categories.

In "Explicit Substitutions and Higher-Order Syntax", Neil Ghani, Tarmo Uustalu and Makoto Hamana provide a categorical model of explicit substitutions, a particular case of binding constructors which does not fall in the general theory of binding algebras. Nevertheless, as the authors show, a language containing explicit substitutions is naturally modeled as the initial algebra of a suitable endofunctor over a functor category.

Fabio Gadducci, Marino Miculan and Ugo Montanari in "About permutation algebras, (pre)sheaves and named sets" investigate the relationships amongst some approaches recently proposed as general models for calculi with names: (pre)sheaf categories, nominal sets, permutation algebras and named sets. This study allows techniques and constructions to be transferred from one model to the other.

The paper "Pseudo-Distributive Laws and Axiomatics for Variable Binding" by Miki Tanaka and John Power provide a general category theoretic formulation of the substitution structure underlying many category theoretic studies of variable and name bindings. The central construction is that of a pseudo-distributive law between 2-monads on Cat, which suffices to induce a suitable substitution monoidal structure.

Finally, we would like to express our gratitude to the rest of the Program Committee of MERLIN 2003 (Simon J. Ambler, Marino Miculan, Dale Miller, Ugo Montanari, Tobias Nipkow, Andrew M. Pitts, Carsten Schürmann), and all the referees who have made this special issue possible.