MERλIN 2003
Second ACM SIGPLAN Workshop on
MEchanized Reasoning about Languages with varIable biNding
Program
|
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 error-prone process. In this paper, we present a new approach based on the use of higher-order 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 frequently-occurring tasks including substitution and rewriting strategies. As we show, compiler development in a logical framework can be easier than in a general-purpose 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 ML-like 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 first-order abstract syntax with variable names so that the formalization is close to that of hand-written 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 syntax-directed deductive system. To simplify verification of the CPS transformation for the language extended let-expressions, it was essential to impose that variables are uniquely used in a program.
Mechanising Hankin and Barendregt using the Gordon-Melham 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 Gordon-Melham axioms, as well as the mechanical support I implemented to make some basic tasks more straightforward.
Reasoning on an Imperative Object-based 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
object-based calculus with closures, method overriding, 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
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, Object-based calculi
with side-effects, Logical Frameworks.
12:30–14:15: Lunch
14:15–15:45: Session 2 (Chair: Andy Pitts)
A unified category-theoretic 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 pseudo-distributive law between 2-monads on Cat, which suffices to induce a pseudo-monad 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 MIL-lite.
Representing Reductions of NP-Complete Problems in Logical Frameworks - A Case Study
Under the widely believed conjecture P != NP, NP-complete problems cannot be solved exactly using efficient polynomial time algorithms. Furthermore, any instance of a NP-complete problem can be converted to an instance of another problem in NP in polynomial time. Thus, identifying NP-complete 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 NP-complete problems, we describe a case study involving two well-known NP-complete 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 2-level architecture in the Hybrid system. OLF here is a version of intuitionistic non-commutative second-order linear logic to be used as a meta-language for the verification of the (meta)theory of deductive systems. It is implemented as a meta-interpreter 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 Mini-ML.
A Modal Foundation for Meta-Variables (20 min)
We report on work in progress regarding a foundation for the notion of meta-variable in logical frameworks and type theories. Our proposal is to treat meta-variables as modal variables in a modal type theory, which is logically clean and justifies several low-level implementation techniques for meta-variables. 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 higher-order 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 first-order theories.
Swapping the Atom: Programming with Binders in Fresh O'Caml (10 min)
We describe Fresh O'Caml, a metalanguage designed to correctly manipulate object-level syntax involving-convertible 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