Home

Engineering Formal Metatheory

Aydemir, Charguéraud, Pierce, Pollack, and Weirich. Engineering Formal Metatheory.

Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitions and theorems that make a huge cumulative difference in the difficulty of carrying out large formal developments. The representation and manipulation of terms with variable binding is a key issue.

We propose a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductive definitions of relations on terms (typing, reduction, . . . ).

...

We have carried out several large developments in this style using the Coq proof assistant and have made them publicly available. Our developments include type soundness for System F<: and core ML (with references, exceptions, datatypes, recursion, and patterns) and subject reduction for the Calculus of Constructions.

A fairly recent paper from the POPLmark team, which describes an approach to formalizing programming metatheory that they think performs well on the POPLmark challenge criteria (low formalization overhead, low cost of entry, and reasonable similarity to existing informal proof techniques). It looks like this is related to some of the material presented in the How to write your next POPL paper in Coq tutorial at POPL'08, which was previously mentioned on LtU.

By Allan McInnes at 2008-01-10 04:54 | Theory | other blogs | 8693 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Yep

This paper does elaborate on the approach used in the tutorial at POPL '08, which, by the way, was wonderful. I'll have to write more about that when the bleeding from my ears stops, but for now, suffice it to say that it was wonderful to meet everyone from the Penn team, Dave Herman, and Adam Chlipala, who sat next to me and was incredibly patient with my brain-dead questions.

By Paul Snively at Thu, 2008-01-10 07:09 | login or register to post comments

Nominal Isabelle

I m not completely convinced about their argument of the Nominal Isabelle:
"....However it is based on a great
deal of bespoke infrastructure only available in Isabelle/HOL, there
are some syntactic restrictions, and certain aspects of formalization
(such as rule inversion and recursive definition over terms) are not well supported...."

I think the Nominal Isabelle is so far the best approach to deal with variable binding. At the end of the day we want an approach that make it as easy as possible to formalise informal proofs about calculi(or programming languages) with binding variables.

By Teme at Sat, 2008-01-12 16:11 | login or register to post comments

Convergence

I can't help but feel that you omitted some crucial context. Worse, it's the context covered by your ellipsis, i.e. immediately before and after the part that you quote:

The nominal package involves no axiomatic extension to Isabelle/HOL, hence is as safe as Isabelle/HOL itself. This nominal representation is a serious alternative to our style for users who want to do formal metatheory. However it is based on a great deal of bespoke infrastructure only available in Isabelle/HOL, there are some syntactic restrictions, and certain aspects of formalization (such as rule inversion and recursive definition over terms) are not well supported (at time of writing) because of the need to respect alpha equivalence.

It seems to me that Section 4.6 of the paper is quite fair to Nominal Isabelle on balance; I encourage interested parties, of course, to read the whole paper, but Section 4.6 is less than a page long, for those short on time and/or patience.

I would also refer you to Section 5.1 of A Mechanized Bisimulation for the Nu-Calculus (PDF), "Semantics of the ν-calculus:"

There has been much recent research effort expended on reducing the pain of doing mechanized reasoning about syntax involving binders, most notably under the umbrella of the POPLmark challenge [3]. We were pleased to find that this effort is paying off: our formalization uses a Coq framework for ‘locally nameless’ reasoning about binding due to Aydemir et al.[2], which worked very well.

The locally nameless style uses de Bruijin indices for bound identifiers and names for free variables. The benefit of this representation is that each alpha equivalence class has a unique representation. A further feature of the framework is the use of cofinite quantification for free variables; the definitions and tactics provided by Aydemir et al. make it very convenient to generate fresh variable names whenever they are required in proofs.

This is, of course, not definitive. Dealing with binding is one, admittedly important, aspect of programming language metatheory, but the lot taken together no doubt will suggest entirely different tools and techniques to different people, which as far as I'm concerned is as it should be. One of the gratifying aspects of attending the Coq tutorial at POPL '08 was precisely to see how many people attending had prior experience with other systems (my favorite overheard comment: "If you ever go into Twelf and need a library for working with rationals, let me know...", which was said to a gentleman with Isabelle experience).

By Paul Snively at Sat, 2008-01-12 23:43 | login or register to post comments