MERλIN 2003

8:45–9:00: Welcome (Furio Honsell)
9:00–10:00: Invited talk (Chair: Furio Honsell)
Scope, binding, and inlining in the Glasgow Haskell Compiler
10:00–10:30: Coffee Break
10:30–12:30: Session 1 (Chair: Dale Miller)
Compiler Implementation in a Formal Logical Framework
The task of designing and implementing a compiler can be a difficult and errorprone process. In this paper, we present a new approach based on the use of higherorder abstract syntax and term rewriting in a logical framework. All program transformations, from parsing to code generation, are cleanly isolated and specified as term rewrites. This has several advantages. The correctness of the compiler depends solely on a small set of rewrite rules that are written in the language of formal mathematics. In addition, the logical framework guarantees the preservation of scoping, and it automates many frequentlyoccurring tasks including substitution and rewriting strategies. As we show, compiler development in a logical framework can be easier than in a generalpurpose language like ML, in part because of automation, and also because the framework provides extensive support for examination, validation, and debugging of the compiler transformations. The paper is organized around a case study, using the MetaPRL logical framework to compile an MLlike language to Intel x86 assembly. We also present a scoped formalization of x86 assembly in which all registers are immutable.
Verifying CPS transformations in Isabelle/HOL
We have verified several versions of the CPS transformation in Isabelle/HOL. In our verification we adopted firstorder abstract syntax with variable names so that the formalization is close to that of handwritten proofs and compilers. To simplify treatment of fresh variables introduced by the transformation, we introduced abstract syntax parameterized with the type of variables. We also found that the standard formalization of αequivalence was cumbersome for theorem provers and reformulated αequivalence as a syntaxdirected deductive system. To simplify verification of the CPS transformation for the language extended letexpressions, it was essential to impose that variables are uniquely used in a program.
Mechanising Hankin and Barendregt using the GordonMelham axioms
I describe the mechanisation in HOL of some basic λcalculus theory, using the axioms proposed by Gordon and Melham [GM96]. Using these as a foundation, I mechanised the proofs from Chapters 2 and 3 of Hankin [Han94] (equational theory and reduction theory), followed by most of Chapter 11 of Barendregt [Bar84] (residuals, finiteness of developments, and the standardisation theorem). I discuss the ease of use of the GordonMelham axioms, as well as the mechanical support I implemented to make some basic tasks more straightforward.
Reasoning on an Imperative Objectbased Calculus in Higher Order Abstract Syntax
We illustrate the benefits of using Natural Deduction in combination
with weak Higher Order Abstract Syntax for formalizing an
objectbased calculus with closures, method overriding, types with
subtyping, and sideeffects, 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
this formalization and the Theory of Contexts, we can prove formally
the Subject Reduction Theorem in the proof assistant Coq, with
relatively small overhead.
Keywords: Interactive theorem proving, Logical foundations of
programming, Program and system verification, Objectbased calculi
with sideeffects, Logical Frameworks.
12:30–14:15: Lunch
14:15–15:45: Session 2 (Chair: Andy Pitts)
A unified categorytheoretic approach to variable binding
We give a general category theoretic formulation of the approach to modelling variable binding first proposed by Fiore, Plotkin, and Turi. This general formulation allows us to include variable binding as they have it, as well as Tanaka's linear variable binding and variable binding for other binders and for mixtures of binders as for instance in the Logic of Bunched Implications. The key structure developed by Fiore et al was a substitution monoidal structure, from which their formulation of binding was derived; so we give an abstract formulation of a substitution monoidal structure, then, at that level of generality, derive the various category theoretic structures they considered. The central construction we use is that of a pseudodistributive law between 2monads on Cat, which suffices to induce a pseudomonad on Cat, and hence a substitution monoidal structure on the free object on 1.
A Definitional Approach to Primitive Recursion over Higher Order Abstract Syntax
It is well known that there are problems associated with formal systems which attempt to combine higher order abstract syntax (HOAS) with principles of induction and recursion. We describe a formal system, called Bsyntax, which we have implemented in Isabelle HOL. Our contribution is to prove the existence of a combinator for primitive recursion with parameters over HOAS. The definition of the combinator is facilitated by the use of terms with infinite contexts, and this new approach addresses the problems of more traditional accounts. In particular, our work is purely definitional, and is thus consistent with classical logic and choice. An immediate payoff is that we obtain higher order substitution for free. We give a presheaf model of Bsyntax, which provides additional semantic validation of Bsyntax's principles of recursion. We outline an application of our work to mechanized reasoning about the compiler intermediate language MILlite.
Representing Reductions of NPComplete Problems in Logical Frameworks  A Case Study
Under the widely believed conjecture P != NP, NPcomplete problems cannot be solved exactly using efficient polynomial time algorithms. Furthermore, any instance of a NPcomplete problem can be converted to an instance of another problem in NP in polynomial time. Thus, identifying NPcomplete problems is very important in algorithm design and can help computer scientists and engineers redirect their efforts towards finding approximate solutions to these problems. As a first step towards a digital library for NPcomplete problems, we describe a case study involving two wellknown NPcomplete problems 3SAT and CHROMATIC together with a reduction and the corresponding soundness proof in a logical framework.
15:45–16:15: Tea Break
16:15–17:55: Session 3 (Chair: Simon Ambler)
A Formalization of an Ordered Logical Framework in Hybrid with Applications to Continuation Machines (20 min)
We report on work in progress devoted to the formalization of an Ordered Logical Framework (OLF) based on a 2level architecture in the Hybrid system. OLF here is a version of intuitionistic noncommutative secondorder linear logic to be used as a metalanguage for the verification of the (meta)theory of deductive systems. It is implemented as a metainterpreter on top of the Hybrid system, which provides the full HOAS language. We apply the framework to the formal verification of type preservation of a simple continuation machine for MiniML.
A Modal Foundation for MetaVariables (20 min)
We report on work in progress regarding a foundation for the notion of metavariable in logical frameworks and type theories. Our proposal is to treat metavariables as modal variables in a modal type theory, which is logically clean and justifies several lowlevel implementation techniques for metavariables. We also speculate on other logical extensions of our modal type theory, at present without clear applications.
Explicit Substitutions and Higher Order Syntax (20 min)
Recently there has been a great deal of interest in higherorder syntax which seeks to extend standard initial algebra semantics to cover languages with variable binding by using functor categories. The canonical example studied in the literature is that of the untyped λcalculus which is handled as an instance of the general theory of binding algebras, cf. Fiore, Plotkin, Turi. Another important syntactic construction is that of explicit substitutions. The syntax of a language with explicit substitutions does not form a binding algebra as an explicit substitution may bind an arbitrary number of variables. Nevertheless we show that the language given by a standard signature Σ and explicit substitutions is naturally modelled as the initial algebra of the endofunctor Id + F_{Σ}o_ + _o_ on a functor category. We also comment on the apparent lack of modularity in syntax with variable binding as compared to firstorder theories.
Swapping the Atom: Programming with Binders in Fresh O'Caml (10 min)
We describe Fresh O'Caml, a metalanguage designed to correctly manipulate objectlevel syntax involvingconvertible names and binding operations. The language extensions made to Objective Caml are surveyed from a practical perspective and the implementation details are briefly discussed.
Reasoning about Recursive Procedures with Parameters
In this paper we extend the model of program variables
from the Refinement Calculus in order to be able to reason more
algebraically about recursive procedures with parameters and local variables.
We extend the meaning of variable substitution or freeness from
the syntax to the semantics of program expressions. We give a predicate
transformer semantics to recursive procedures with parameters and prove
a refinement rule for introduction of recursive procedure calls. We also
prove a Hoare total correctness rule for our recursive procedures. These
rules have no side conditions and are easier to apply to programs than
the ones in the literature. The theory is built having in mind mechanical
verification support using theorem provers like PVS or HOL.
Key words: Refinement, Recursive procedures, Semantics, Hoare rules