|

 

Rnyingma.synrc.com

Engineering Formal Metatheory Arthur Chargu´eraud Benjamin C. Pierce University of Pennsylvania University of Pennsylvania Stephanie Weirich University of Edinburgh University of Pennsylvania rem proving; D.3.1 [Programming Languages]: Formal Defini- Machine-checked proofs of properties of programming languages tions and Theory—Syntax have become a critical need, both for increased confidence in largeand complex designs and as a foundation for technologies such as Design, Documentation, Languages, Theory, Ver- proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitionsand theorems that make a huge cumulative difference in the diffi- binding, Coq, locally nameless culty of carrying out large formal developments. The representationand manipulation of terms with variable binding is a key issue.
We propose a novel style for formalizing metatheory, combin- ing locally nameless representation of terms and cofinite quantifi- Recent years have seen burgeoning interest in the use of proof as- cation of free variable names in inductive definitions of relations on sistants for formalizing definitions of programming languages and terms (typing, reduction, . . ). The key technical insight is that our checking proofs of their properties. However, despite several suc- use of cofinite quantification obviates the need for reasoning about cessful tours de force (Appel 2001; Crary 2003; Klein and Nipkow equivariance (the fact that free names can be renamed in deriva- 2006; Leroy 2006; Lee et al. 2007, etc.), the community remains tions); in particular, the structural induction principles of relations fragmented, with little synergy between groups and, for newcom- defined using cofinite quantification are strong enough for metathe- ers wanting to join the game, a perplexing array of choices between oretic reasoning, and need not be explicitly strengthened. Strong different logics, proof assistants, and representation techniques.
inversion principles follow (automatically, in Coq) from the induc- To stimulate progress on this problem, Aydemir et al. (2005) tion principles. Although many of the underlying ingredients of our proposed the POPLMARK challenge, a set of tasks designed to technique have been used before, their combination here yields a stress many of the critical issues in formalizing programming significant improvement over other methodologies using first-order language metatheory. They laid out three criteria for evaluat- representations, leading to developments that are faithful to infor- ing proposed formalization techniques: infrastructure overhead— mal practice, yet require no external tool support and little infras- formalization overheads, such as additional operations and their tructure within the proof assistant.
associated proof obligations, should not be prohibitive for large We have carried out several large developments in this style us- developments; transparency—formal definitions and theorems ing the Coq proof assistant and have made them publicly avail- should not depart radically from the usual informal conventions able. Our developments include type soundness for System F<: familiar to a technical audience; and cost of entry—the infrastruc- and core ML (with references, exceptions, datatypes, recursion, and ture should be usable by someone who is not an expert in theorem patterns) and subject reduction for the Calculus of Constructions.
prover technology.
Not only do these developments demonstrate the comprehensive- In this paper, we propose a new style for formalizing program- ness of our approach; they have also been optimized for clarity and ming language metatheory that performs well on all these criteria.
robustness, making them good templates for future extension.
The style builds upon two key ingredients: locally nameless repre-sentation of syntax involving binders and a cofinite style of quan- Categories and Subject Descriptors F.4.1 [Mathematical Logic tification for introducing free names in rules dealing with binders.
and Formal Languages]: Mathematical Logic—Mechanical theo- In locally nameless representation, bound variables are repre- sented by de Bruijn indices while free variables are represented bynames. This mixed representation combines the benefits of both ap-proaches, avoiding difficulties associated with alpha-conversion byensuring that each alpha-equivalence class of terms has a uniquerepresentation, while supporting formal reasoning that closely fol-lows informal practice.
The second ingredient is the use of a cofinite quantification of ACM, 2008. This is the author's version of the work. It is posted here by permission free names introduced by rules dealing with binders, instead of the of ACM for your personal use. Not for redistribution. The definitive version will appear standard "exists-fresh" quantification—these styles are illustrated in the proceedings of POPL 2008.
by the following variants of the typing rule for abstraction in the simply-typed lambda calculus (λ→): mantics. Section 4, the technical meat of the paper, describes theproblem faced by the exists-fresh specification, shows how cofi- ∈ FV(t) E, x:S tx : T nite quantification solves this problem, and discusses why our so-lution is significantly better than other concrete approaches. Fi- nally, Section 5 gives a practical overview of our larger formaliza- Here, tx is the body of abstraction (abs t) opened up with a free tions. This section also quantitatively compares our developments variable named x. In the second rule, L is some finite set of to each other and to other publicly available Coq solutions to the names that is chosen when we apply the rule. Just as EXISTS- POPLMARK challenge.
FRESH is applicable if there exists some x / ∈ FV(t) such that tx : T , so COFINITE is applicable if there exists A Survey of Binding Representations some L such that ∀x / ∈ L. E, x:S tx : T . The induction There are two main categories of approaches to representing and hypothesis for rule EXISTS-FRESH holds for one particular name reasoning about syntax with binding, depending on whether vari- x, which (notionally) comes from the derivation being eliminated ables and binders are represented as concrete nodes in first-order by the induction; if that x is not fresh enough, the only way to algebraic structures or whether these aspects are "lifted to the met- proceed is to reason about equivariance of the typing judgement.
alanguage" by representing the bodies of binding constructs as met- The cofinite rule, on the other hand, asserts from the start that for alanguage functions. In each category there are many ingenious E abs t : S → T to hold there must be infinitely many variations, and we do not attempt to be exhaustive in this survey.
xs with E, x:S tx : T ; surely one of them is fresh enough Outside the main categories, there is a plethora of hybrid represen- since only finitely many names could have been used so far. In rare tations, multi-level representations, . . , which we do not consider.
cases, renaming is necessary for proofs, but it is straightforwardlysupported by the cofinite presentation; the required lemmas may Concrete Approaches be easily derived from standard properties such as substitution With concrete (or first-order) approaches, variables are typically and weakening, which are themselves derivable using only the encoded using names or natural numbers. Capture-avoiding substi- cofinite definition. These renaming lemmas also provide the core tution must then be defined explicitly as a function on terms, and arguments for the equivalence between the exists-fresh and cofinite in the case where bound variables are named, alpha-equivalence presentations of the relations.
must also be defined explicitly. Concrete approaches can be subdi- Neither of these ingredients is entirely new. The locally name- vided roughly in three categories: those using names to represent less representation dates back to the introduction of de Bruijn in- variables, those using de Bruijn indices, and those distinguishing dices. Several strengthened induction principles that avoid manual bound and free variables (which may use either names or indices renaming have been proposed (Gordon 1994; McKinna and Pol- for each kind of variable).
lack 1993, 1999; Urban et al. 2007b). The idea of reasoning about The most standard representation on paper uses names to rep- the freshness of names by considering all but those in some finite resent variables, generally quotienting raw expressions by some set is at the heart of nominal logic (Pitts 2003) and also appears notion of alpha-equivalence. Although used since the first days of in definitions of alpha-equivalence by Krivine (1990) and Ford and the lambda calculus, this representation has not proved convenient Mason (2001). Our contribution lies in the precise way that we for formal developments. For example, naive substitution is not combine and apply these ingredients. In particular, the cofinitely structurally recursive in this setting but requires well-founded re- quantified typing rule for abstraction (presented earlier), which re- cursion. Nevertheless, the Church-Rosser property in pure lambda flects both key aspects of our design, does not appear in prior work.
calculus has been proved using named representations by Home- The observation that we can use this formulation to derive renaming ier (2001) using HOL, Ford and Mason (2001) using PVS, and lemmas with little infrastructure is a key point, of both theoretical Vestergaard and Brotherston (2003) using Isabelle/HOL (unusu- and practical interest.
ally, Vestergaard and Brotherston reason about unquotiented raw To demonstrate the comprehensiveness of our approach we have terms). Other attempts to tame this representation include work by developed several significant examples in the Coq proof assis- Stoughton (1988), where simultaneous substitution is defined struc- tant (Coq Development Team 2007): proofs of type soundness for turally and puts terms into a canonical alpha-normal form, and by λ→, System F<: (the core of the POPLMARK challenge—parts 1A Hendriks and van Oostrom (2003).
and 2A), and ML extended with references, exceptions, datatypes, To overcome the clumsiness of explicit alpha-conversion or recursion and patterns, as well as a proof of subject reduction for quotienting, the first large formalizations of languages with binders the Calculus of Constructions (including a proof of the Church- were based on de Bruijn indices (1972) rather than names. In Rosser property). These developments require no external tool sup- this approach, each alpha-equivalence class of lambda-terms has a port and could be reproduced with another general purpose theo- unique syntactic representation in which variables are encoded us- rem prover. Little infrastructure is required between the statement ing natural numbers giving the depth of the variable relative to its of the system formalized and the core of the formal reasoning. Fur- binder. Indices greater than the number of enclosing local binders thermore, our formal reasoning faithfully follows informal practice, may indicate a position in some enclosing context such as a typing preserving the skeletons of proofs and the kinds of arguments in- context. There is abundant evidence of the effectiveness of this rep- volved, unpolluted by details about alpha-conversion or freshness.
resentation, from proofs of the Church-Rosser property for lambda We have carefully organized and commented these proof scripts calculus—for example, by Shankar (1988) using the Boyer-Moore and made them freely available as starting points for comparison prover, by Huet (1994) in Coq, by Rasmussen (1995) in Isabelle/ZF, and by Nipkow (2001) in Isabelle/HOL—to harder results such as The paper is organized as follows. Section 2 surveys possible strong normalization for System F in LEGO (Altenkirch 1993) and approaches to representing binding structures, locates the locally formalizing Coq in Coq (Barras and Werner 1997). In de Bruijn nameless approach in this space, and sketches its history. Section 3 representation, the treatment of bound variables incurs minor tech- presents a complete specification of λ→ using locally nameless nical annoyances (lifting over binders, etc.), while the treatment of representation and the standard exists-fresh presentation of the se- free variables (e.g., variables bound by a typing context) requiresreasoning far from natural informal presentations. For example, consider the statement of a lemma that says thinning the typing context (weakening and permuting) preserves a judgement: indices stract "axiomatic" representation of named terms. Pollack (2006) occurring in the judgement must be updated to match the permuta- has more recently emphasized the benefits of locally nameless rep- tion of their binding points in the context.
resentation in the context of the POPLMARK challenge. Locally Nominal logic (Pitts 2003) provides another way to address the nameless representation with (variants of) McKinna–Pollack style problem of alpha-conversion inherent in the named representation.
reasoning has been used by several researchers (with several proof Urban (2007) and Urban et al. (2007a,b) have adapted these ideas tools) for solutions to the POPLMARK challenge, first by Leroy to standard higher-order logic, and are developing a nominal pack- (2007) and later by Chlipala (2006) and Ricciotti (2007).
age in Isabelle/HOL that provides facilities for formal reasoningwith binders over names. The package helps by automating lan- Higher-Order Approaches guage definitions that equate alpha-equivalent terms, by provid- Higher-order representations use the function space of the meta- ing lemmas about renaming and freshness of names, by deriving logic to encode binding in an object language, allowing issues like strengthened induction principles that provide name freshness facts capture-avoidance and alpha-equivalence to be handled once and for relations over these languages, and by supporting recursion over for all by the meta-logic, rather than facing them anew for each these languages. Some syntactic restrictions must be observed to object language. There is a bewildering variety of higher-order use this package. See Section 4.6 for further discussion of the nom- approaches, which we survey only superficially.
inal package.
In higher-order abstract syntax (HOAS) (Harper et al. 1993; Besides these "homogeneous" concrete approaches—where Pfenning and Elliot 1988), the introduction form for lambda- there is a single notion of "variable," either a name or a de Bruijn abstractions has type (term->term)->term, i.e., the lambda con- index—there is a third category of concrete representations that structor packages a function of type (term->term), which should uses two distinct syntactic classes, called variables (for locally be thought of as the function substituting its argument into the bound variables) and parameters (for free, or globally bound vari- body of the lambda. Not only are alpha-equivalent terms equal, but ables). The idea that variables and parameters should be distin- substitution is handled by the meta-language.
guished goes back at least to Gentzen (1969) and Prawitz (1965).
HOAS was introduced by Church and developed by de Bruijn, Several combinations can be considered, using names, indices, or Martin-L¨of, Plotkin, Pfenning, and their co-workers. The modern levels to represent bound and free variables; of these, two have form, using dependent types and hypothetical and schematic judge- been used in the literature.
ments as well as HOAS term representation, appeared in the Edin- The first is the locally named representation, which uses dis- burgh Logical Framework (LF) (Harper et al. 1993). By design, tinct species of names to represent variables and parameters respec- LF is a weak type theory to be used as a metalanguage, not sup- tively. McKinna and Pollack introduced this technique to formal- porting inductive definition or primitive recursion. It allows faithful ize Pure Type Systems (PTS) (1993; 1999), following a suggestion representation of object languages, where LF itself adds no math- by Coquand (1991). This representation avoids the difficulties of ematical strength to the object language representation. The use reasoning about capture-avoiding substitutions: since variables and of LF methodology for metatheory (as opposed to just representa- parameters are syntactically distinguished, no parameter can ever tion) has been highly developed by Pfenning and his co-workers; be captured by a variable binder during substitution. McKinna and the implementation of this approach is the Twelf system (Pfenning Pollack also introduced a technique for handling the requirement of and Sch¨urmann 1999), which is widely used and very successful choosing fresh global variables that often occurs in reasoning about for formalizing the metatheory of a wide variety of programming binding (weakening lemmas are a prototypical example of the prob- languages (Ashley-Rollman et al. 2005; Lee et al. 2007). The ap- lem). By careful choice of definitions, they avoid the need to reason proach continues to be developed foundationally as well as in prac- about alpha-equivalence of bound variables throughout their large tice (Harper and Licata 2007).
formal body of PTS metatheory. With these techniques, reasoning A second main stream of work, weak higher-order encodings, about lambda calculus and type theory is straightforward, if heavy.
gives a type such as (name->term)->term to the lambda con- Nonetheless, the use of names for bound variables is not a per- structor of terms.2 This constructor packages a function of type fect fit to the intuitive notion of binding: eventually one needs to (name->term), which should be thought of as a function that takes reason about alpha-conversion. For example, parallel reduction has a name and returns the instance of the lambda's body instantiated the diamond property concretely in locally named representation, with that name. Here, alpha-equivalent terms are equated, but sub- but beta reduction has this property only up to alpha-conversion stitution must be defined as a relation between terms. Despeyroux (Pollack 1994b, Section 3.3.6). So Pollack (1994a) suggested that et al. (1995) demonstrate an early use of this approach. The ap- the McKinna–Pollack approach to reasoning with two species of proach has been most developed by Honsell, Miculan, and their variables also works well with a representation that uses names co-workers as the Theory of Contexts (Honsell et al. 2002; Bucalo for parameters and de Bruijn indices for bound variables. This lo- et al. 2006).
cally nameless representation, in which alpha-equivalence classeshave canonical representation, was already mentioned in the con- Why Locally Nameless? clusion of de Bruijn's famous paper (1972). It had been used for We have chosen to concentrate on concrete approaches to repre- implementation in Huet's Constructive Engine (1989), and later in sent binding structure. Despite the attractiveness of higher-order the implementations of the Coq, LEGO (Luo and Pollack 1992), approaches and their demonstrated success in many large develop- HOL 4 (Norrish and Slind 2007), Isabelle, and EPIGRAM (McBride ments, they are, at present, not completely general-purpose. Twelf and McKinna 2004) proof assistants.
is currently the only industrial-strength proof assistant for devel- In the context of formal proofs, Gordon (1994) appears to be the first to have used locally nameless representation. Rather than 2 The technical advantage of the weak variant is that the type of terms can reason directly with locally nameless terms, he builds a represen- be given as an inductive datatype. For strong HOAS, due to the negative oc- tation of named lambda terms on top of locally nameless terms currence of term in (term->term)->term, there is no inductive datatype and demonstrates how the named terms may be used as a basis representing the set of terms. In the weak version, on the other hand, the for representing syntax. Using this technique, Gordon formalized type name replaces the negative occurrence of term, so there is a datatype Abramsky's lazy lambda calculus. Later work by Gordon and Mel- of weak higher-order terms in, e.g., Coq and HOL. Nonetheless technical ham (1996) also uses locally nameless terms as a model for an ab- problems arise unless name is a sufficiently abstract type (Honsell et al.
2002).
oping metatheory based on HOAS representations, and it is (in itscurrent incarnation) strictly limited in its proof-theoretic strength.
The Theory of Contexts is also interesting, but hasn't yet been takenup beyond its originators. These are the subject of active research and may become more generally applicable in the future.
Among the concrete approaches, locally nameless representa- bvar i fvar x app t tion offers the best combination of features. Because free variables are represented using names, lemmas are stated and proofs struc- tured just as they are with the standard representation using names, Open: tu ≡ {0 → u} t, with making locally nameless developments intuitive. In particular, theshifting operations that clutter both statements and proofs in a pure {k → u} (bvar k) de Bruijn setting are avoided. Because bound variables are repre- {k → u} (bvar i) sented using indices, each alpha-equivalence class of lambda terms {k → u} (fvar x) has a unique representation, thus avoiding the difficulties associated {k → u} (app t1 t2) app ({k → u} t1) ({k → u} t2) with alpha-equivalence. Finally, because bound and free variables {k → u} (abs t) abs ({(k + 1) → u} t) are syntactically distinguished there is no issue of variable capture, and substitution can be defined by simple structural recursion.
These observations motivate the choice of the locally nameless representation. The next section presents this style in detail.
FV(t1) ∪ FV(t2) Locally Nameless Representation Locally closed terms: In this section, we describe locally nameless representation, usingλ→ as a running example. All the material presented is formal, in the sense that we have implemented it in Coq.3 We write ⇒ for The fundamental idea of the locally nameless approach is to dis- Well-formed environments (no duplicate names): tinguish bound from free variables, using de Bruijn indices for theformer and names for the latter. Figure 1 presents a locally name- less specification of λ →. An occurrence of a bound variable is rep- resented as (bvar i) where i is a natural number index denoting thenumber of enclosing lambda abstractions that must be traversed be- fore reaching the abstraction binding that variable. Abstractions do not bind names; for example, (abs (bvar 0)) is the identity func- In its raw form, this representation is not isomorphic to ordinary named lambda terms because a bound variable may not resolve to any binder. For example, (abs (bvar 2)) does not represent anylambda-term. We therefore define a predicate, (term t), on pre- terms (the syntactic objects defined by the grammar in Figure 1) that selects the locally closed pre-terms—or just terms—in which all indices resolve to binders.
The key operation on pre-terms is opening an abstraction by in- stantiating a bound variable with a term. If (abs t) is an abstraction and u another term, then the result of opening the abstraction withu, written tu, is formed by replacing in the body t all bound vari- ables that point to the outermost lambda with u. Figure 1 gives the app (abs t) u 7−→ tu structurally recursive definition of the open function; the idea is toexplore the term, keeping track of the current number of binders passed through.4 One use of the open operation is in the conclusion of the beta reduction rule, RED-BETA, near the bottom of the figure.
1 t2 7−→ app t01 t2 The open operation is also frequently applied to a free variable; we call this specialized version variable opening, which we write with abuse of notation as (tx) instead of (tfvar x). Variable opening app t1 t2 7−→ app t1 t02 is used when passing through a binder to turn the bound variable Type soundness lemmas (preservation and progress): into a free variable. In a named representation, we may have our hands on an abstraction (abs x t) and wish to talk about its bodyt. With the locally nameless representation, the abstraction would (value t ∨ ∃t0, t 7−→ t0) 3 The corresponding development is contained in files STLC Core *.v.
Figure 1. Locally nameless presentation of λ→ 4 Experts will note that this definition of open works correctly only whenzero is the only unbound index. The definition can be generalized to allowmultiple binders to be opened simultaneously as explained in Section 5 inthe paragraph about our ML development.
be written (abs t); to talk about its body as a term (rather than a Substitution of a term for a free name: pre-term with an unbound index), we open t with some fresh name [z → u] (bvar i) x. A typical example of variable opening appears in the typing rule [z → u] (fvar z) for abstractions, TYPING-ABS.
[z → u] (fvar x) In variable opening, the chosen variable should not already [z → u] (app t1 t2) app ([z → u] t1) ([z → u] t2) appear free inside the term. Otherwise, the operation would be a [z → u] (abs t) abs ([z → u] t) form of variable capture: the name being given to the index, abound variable, would be the same as a free variable. Therefore, Properties of substitution: the rule TYPING-ABS also includes the premise x / ∈ FV(t),5 which ∈ FV(t) ⇒ [x → u] t = t uses the free variable function to collect the set of free variables in [x → u] (tw) = ([x → u] t)([x→u] w) a pre-term. Like open, this function is defined by simple structural recursion and need not worry about confusing free and bound [x → u] (ty) = ([x → u] t)y variables—all variable names in the term are free, since bound when x 6= y and term u variables are represented by indices.
[x → u] (tx) = tu To state the typing judgement of λ→, we need to formalize typing environments. In Figure 1, environments are concretelyrepresented as association lists, for which we assume some stan- Figure 2. Substitution dard operations. The concatenation of two environments is written(E, F ). The lookup of a variable in an environment is expressed bythe predicate (x:T ) ∈ E, which holds when (x, T ) is the rightmostpair of E whose first component is x. Finally, a variable is fresh Close: xt ≡ {0 ← x} t, with for an environment, written x / ∈ dom(E), when that variable does not appear in the first component of any pair in E. In principle, the {k ← x} (bvar i) association list representation allows multiple assumptions for the {k ← x} (fvar x) same variable, but our typing rules ensure that environments partic- {k ← x} (fvar y) ipating in derivable judgements are well formed (ok) in the sense {k ← x} (app t1 t2) app ({k ← x} t1) ({k ← x} t2) that a given variable is bound at most once in a given environment.
{k ← x} (abs t) abs ({(k + 1) ← x} t) The final portion of Figure 1 completes the definition of λ→ by stating the properties we wish to prove: the standard preservation Figure 3. Variable Closing and progress lemmas. The figure, as a whole, forms our "trustedbase" of definitions: one must believe in the correctness of every-thing stated in the figure in order to believe that a formal proof oftype soundness is really about one's informal notion of λ Working With Local Closure discuss this issue in additional detail in Section 3.4.
We use an inductive definition of local closure, given in Figure 1. Abound variable on its own is never locally closed: there is no case for (bvar i). An abstraction is locally closed if the body of thatabstraction, once opened up with a fresh name, is locally closed.6 The definition of λ→ depends only on the open and FV operations.
There are alternative ways to define local closure, but we favor In proofs, however, the operation of free variable substitution, this style which is similar to the VClosed relation of McKinna replacing free names with terms, is also needed. Written [x → u] t, and Pollack (1993). As they point out, this definition provides a it is defined by structural recursion in Figure 2. As in the definition structural induction principle for locally closed terms: of open, there is no arbitrary choice of name for the bound variablein the abstraction case, so we need not worry that this choice will affect the result. Therefore, the behavior of substitution is natural ∀ t1 t2. P (t1) ⇒ P (t2) ⇒ P (app t1 t2) and easy to reason about.
∈ FV(t) ⇒ P (tx) ⇒ P (abs t) The properties of the substitution function, shown in the bottom ∀t. term t ⇒ P (t) portion of Figure 2, are fundamental when working with a locallynameless representation. Lemma subst fresh states that substitu- This definition can be used in many different logics: intensional or tion for an unused variable has no effect, and lemma subst open extensional, dependent types or simply typed HOL.7 states that substitution distributes over the opening operation. The Although the relations defining the semantics of λ→ in Figure 1 remaining two lemmas are immediate corollaries of the former are formally defined over pre-terms, these relations actually include two. Lemma subst open var permutes a substitution with variable only locally closed terms and the basic operations preserve local opening, and lemma subst intro decomposes an open operationinto a variable opening operation and a substitution. Examples of when these lemmas are used can be found in the proof of the substi- The freshness assumption is not actually required for this judgement; we include it to maintain the invariant that a term is never opened with a name tution lemma for λ→ (Section 4.1) and in the proof of a renaming that occurs free in that term.
lemma (Section 4.2).
We occasionally need a related operation—intuitively, a recip- In extensional higher order logic the (non-empty) predicate term can be made into a type of locally closed terms. In intensional dependent type rocal of variable opening—that abstracts the name x from the term systems (including Coq), this construction isn't available. However, in such t, replacing it with a bound variable. We call this operation variable systems we can define the inductive family of pre-terms indexed by the set closing and define it in Figure 3, again by structural recursion.
of bvars occurring free (e.g. McBride and McKinna (2004); for discussionof inductive families see Dybjer (1994)). Then the section of this familyindexed by the empty set of bvars is exactly the locally closed terms.
5 The rule TYPING-ABS could also explicitly include a premise to ensure Improvements to our style may be possible along these lines, but for the that x does not appear in the domain of the environment E. However, that moment we stick with the representation given above, for its simplicity of restriction is already implied by the second hypothesis.
use and uniformity of presentation across different logics.
for theorems versus adequacy for derivations.) In our setting, you term (abs t) ∧ term u ⇒ term (tu) can carry this out (on paper, not in Coq) with a fairly simple term u ∧ term t ⇒ term ([x → u] t) ⇒ term t ∧ term t0 Cofinite Quantification We formulate the definitions in this way for two reasons. First, it is Although the definitions in the previous section adequately repre- required for the adequacy of our formalization: only locally closed sent λ→, they yield insufficiently strong induction principles: in terms correspond to alpha-equivalence classes of ordinary named many situations we must rename the variable used to open an ab- terms. Second, some useful properties of the definitions are true straction to complete a proof. The need to reason about renaming only for locally closed terms.8 The typing relation ensures local motivates our use of "cofinite quantification" for inductively de- closure of its subject without any local closure premises, but not fined relations.
every relation of interest is this clean. For example, to ensure this In this section, we present a complete style of proof devel- property of small-step evaluation, the definition includes several opment based on cofinite quantification. We first explain cofinite local closure premises. In general, such premises are only required quantification and give a new definition of λ→ using it. Defini- at the leaves of the definition: e.g., we do not need a premise tions in this style are sufficient, by themselves, to develop signif- (term t) if there is already a premise (value t), since the latter icant amounts of metatheory—e.g., to prove weakening and sub- implies the former.
stitution results—since they naturally balance strong induction and Similarly, because our definitions guarantee local closure, we inversion principles with useful introduction forms. In a few situa- usually do not need to add local closure hypotheses to the state- tions, however, renaming lemmas are required to build derivations ments of lemmas and theorems. For example, the "substitution pre- using the cofinitely quantified rules. We show how these lemmas serves typing" lemma can be derived directly from weakening and substitution. Finally,to be confident that relations defined with cofinite quantification are adequate encodings of λ →, we use renaming to show that they are equivalent to their counterparts shown in Figure 1.
requires none because the typing relation ensures that t, u, and Having described our complete style of development, we then [z → u] t are all locally closed. As a result, even though the use of observe that some significant streamlining is possible, notably in the nameless representation means that we must be careful about cases where one believes in the adequacy of the cofinite presenta- local closure, the management of this predicate does not require a tion of a relation without requiring a formal proof of equivalence significant departure from common informal practice.
with the "exists-fresh" variant. We conclude the section with com-parisons to previous work, arguing that the added value of our ap- proach is significant in each case.
Why should you believe this mechanized, formal representation ofλ Stronger Induction Principles → is "correct," i.e., expresses your understanding of the rigorous, informal system? This is the question of adequacy of the represen- The definitions of the local closure and typing relations in Figure 1 tation, set out by Harper et al. (1993) in their context of HOAS.
use an "exists-fresh" style of quantification. When an abstraction is (See also (Harper and Licata 2007) for a more recent take.) First, opened in the premise of a rule (TERM-ABS and TYPING-ABS), the note that it is an informal question, because it involves the relation- name used in the premise is required to be fresh for the body of the ship between an informal thing and a formal thing. No matter how abstraction. Thus, to build a derivation using one of these rules, it much faith you put in Coq, no Coq proof will completely settle this suffices to show that there exists a single sufficiently fresh name for which the premise holds. The premises of rules written in this way Nonetheless, formal proofs are useful for this question in three are easy to satisfy, making them ideal introduction forms.
ways. First, you may prove that the formalization has the proper- However, such rules give rise to weak elimination forms (in- ties you expect from the informal system and does not have un- version and induction principles). The fact that the premises of a expected properties. E.g., our Coq representation of λ→ is shown rule defined using exists-fresh quantification need only hold for one to have Church–Rosser, weakening, subject reduction, etc., some particular name means that the corresponding induction hypothesis of which is discussed below. (You must also be convinced that our also holds for one particular name. That name will only be as fresh formal statements of these properties are correct.) If you think our as the premise of the rule requires, which may not be enough.
rule TYPING-ABS requires a stronger side condition, prove your For example, consider the proof of the weakening lemma for expected rule is admissible in our system. Second, you may prove the typing relation, which allows one to insert additional typing some formal relationship with another formalization of the same in- assumptions anywhere into a typing environment: formal system that you, and other readers, believe to be adequate, e.g., that our formalization is related to a pure de Bruijn representa- tion in some way (but we haven't done that). Finally, if intensional, impredicative, constructive type theory is just too weird, you maycarry out the same representation and its development in some other When proving this by induction on the given typing derivation, in proof system. We have avoided using special properties of Coq or the case for TYPING-ABS we are given a derivation ending with its logic, and our style could be carried out in HOL, NuPrl, PVS, Harper et al. (1993) ask that there be a compositional bijection between the informal syntactic entities (terms, formulas, . . ) and and an induction hypothesis some collection of entities of the formal representation. (They also note this may be taken to have different meanings: e.g., adequacy ok (E, F, G, x:T1) ⇒ (E, F, G, x:T1 t1 and we must derive 8 These include both low-level technical properties such as subst open andmore interesting properties such as reflexivity of subtyping in System F<:.
we are given the assumption ∈ L0. (E, G, x:T for some finite set of names L0, and an induction hypothesis termc (app t1 t2) ∈ L0. ok (E, F, G, x:T1) ∈ L. termc (tx) and we must derive E, F, G c abs t1 : T1 → T2 .
By C-TYPING-ABS, it suffices to find an L for which we can show ∈ L. (E, F, G, x:T Choosing L = L0 ∪ dom(F ) does the trick: any x / ∈ L is also not in L0, so the induction hypothesis directly gives us the result.
∈ L. (E, x:T1 c tx : T2) As an additional example of the usefulness of the stronger induction hypothesis, we prove the standard "substitution preservestyping" lemma for the cofinite typing relation: Figure 4. Local closure and typing using cofinite quantification for an arbitrary F . By TYPING-ABS, it suffices to derive The proof of this lemma also demonstrates the ease of working withsubstitution in a locally nameless setting. It proceeds by induction on the given typing derivation for t. In the case for C-TYPING-ABS,we have a derivation that ends in for some name y / ∈ FV(t1). Intuitively, we want to use y = x, since the induction hypothesis applies to x. However, the given ∈ L0. (E, z:S, F, x:T1 c t1 typing derivation shows that t x is well typed in the environment (E, G, x:T1), so we can only derive that x is fresh for (E, G). Weneed to type t x for some finite set of names L0, and an induction hypothesis in the extended environment (E, F, G, x:T1), but x is not guaranteed to be sufficiently fresh for that environment as ∈ L0. (E, F, x:T it could appear in F .
1 c [z → u] (t1 The particular name x appearing in the induction hypothesis is and we must derive (notionally) the name that occurs in that position of the particularderivation of E, G t : T being eliminated in the proof. In an E, F c [z → u] (abs t1) : T1 → T2 .
informal proof, we avoid the problem by assuming this derivation By the definition of substitution, we simplify the substitution to uses sufficiently fresh names. (Depending on our informal view, abs ([z → u] t1). Then to apply C-TYPING-ABS, we must find an this is usually justified by appeal to the Barendregt Variable Con- L for which we can show vention (1984), which allows us to assume that the name of thebound variable in the abstraction case is sufficiently fresh.) ∈ L. (E, F, x:T1 c ([z → u] t1)x : T2) .
Our solution is to strengthen the induction principle for the We use subst open var to write ([z → u] t typing relation by changing its definition to the one at the bottom of 1)x as [z → u] (t1 (to match the induction hypothesis). To do this rewriting, we need Figure 4. This definition differs only in the rule for abstractions, C- x and z to be distinct. Since the induction hypothesis holds only for TYPING-ABS. This new rule intuitively states: "to show that (abs t) ∈ L0, we choose L = L0 ∪ {z}.
is well typed it suffices to choose some finite set of names, L, In this proof and in the proof of weakening, we carefully chose and show that tx is well-typed for every x not in L." We say that this definition of the typing relation uses "cofinite quantification" C-TYPING-ABS to create a new typing derivation.
In practice, we use a tactic to instantiate L with the set of all names since we must show that the premise of C-TYPING-ABS ("C" for appearing in the current proof context: intuitively, showing that a "cofinite") holds for all but finitely many names. The set of names judgement holds for fewer names is easier than showing that it L may be different for each use of the rule. To similarly strengthen holds for more.
the structural induction principle for terms, we redefine term in thecofinite style at the top of Figure 4, and replace all references toterm in the reduction relation with this one. Although this new definition of λ→ differs from the one given in Figure 1, it is There are a few situations in which we need to apply a derivation equivalent, as we show in Section 4.3.
rule with a cofinitely quantified premise but only know that this Using cofinite quantification in the rules provides a stronger premise holds for one particular fresh name. Alternatively, know- induction principle because, in the cases that open abstractions, the ing that an abstraction type checks, we may wish to use inversion induction hypotheses will hold for all names except those in some to show that the body of an abstraction type checks with a particu- finite set L, rather than just for a single name. On the other hand, lar name, but we do not know that that particular name is excluded a rule defined using cofinite quantification is nearly as easy to use from the set L used with that invocation of C-TYPING-ABS. In such for introduction as the exists-fresh version because L can include situations, we need to explicitly invoke the fact that our judgments the finitely many names that could potentially lead to clashes.
are equivariant through a renaming lemma. We present now an ex- Consider again the proof of the weakening lemma—this time, ample of such a situation and explain how to prove the renaming for the cofinite typing relation c. In the case for C-TYPING-ABS, lemma by reusing the corresponding substitution lemma.
Suppose that we are trying to show that type checking is decid- To show (1), we use C-TYPING-VAR. To show (2), we use the weak- ening lemma, by which it suffices to show that E, x:T1 c tx :T typing decidable : 2. This result follows from the assumptions of typing rename.
In our experience, renaming lemmas are rarely needed. Aside from typing decidable, the only situations in our developments We prove this result by induction on term t. Consider the case for where they are required are in the proofs of confluence for beta abstractions (where t = abs t1) with an arbitrary environment E reduction in the lambda calculus and the Calculus of Constructions.
and an arrow type (where T = T1 → T2). Here we are given In these proofs, the conclusion of the theorem is an existential an induction hypothesis that states that type checking the body is statement: "there exists a common reduct. . " The cases which decidable (for some finite set L0).
require renaming involve rules with binding, where we have aninduction hypothesis of the form "for all x not in L0, there exists ∈ L0. ∀ E0 T 0, t such that . . " which we need to use to prove a statement of the : T 0) ∨ ¬(E0 c t1 form "there exists t such that for all y not in L, . . " The induction At this point we must determine whether the body type checks to hypothesis is strictly weaker than the statement we are trying to know whether the abstraction should type check. So we pick an prove. For each name x, it gives us an object t for which some arbitrary fresh variable, x / relation holds. We must use the renaming lemma for that relation 1) ∪ dom(E), and consider the two cases that arise from instantiating E0 with (E, x:T to show that the relation holds for all sufficiently fresh names y.
T 0 with T2.11 If the body does type check, we have a derivation of Equivalence of Exists-Fresh and Cofinite Definitions At this point we have defined two sets of rules for λ→: one con- However, to show that the abstraction type checks, using rule sisting of the original exists-fresh definitions, which corresponds directly to the "paper presentation," and one that uses cofinite quan- TYPING-ABS, we must show that there is some L such that tification, which yields stronger induction principles. To be confi- dent that the cofinite definitions are adequate, we verify (formally)that they define the same relations as the exists-fresh variants.13 Although x was arbitrary, we do not know whether the particular Note that these proofs of equivalence are straightforward conse- variable that we chose influenced whether the body type checked.
quences of renaming lemmas.
Therefore, we complete the proof with the help of a renaming Let us take the typing relation as an example. The theorem to lemma that asserts that typing judgments are stable under certain prove is the following: ∈ (dom(E) ∪ FV(t Both directions are straightforward inductions. The TYPING-ABS ∈ (dom(E) ∪ FV(t case of the ⇐ direction is the only interesting case, where we mustshow (E c abs t1 : T1 → T2) from the induction hypothesis This renaming lemma allows us to go from a typing derivation : T2) and an assumption (x / ∈ FV(t1)). This for a single variable x, to a typing derivation for a cofinite set of case follows by applying C-TYPING-ABS, instantiating L to be variables. Using this lemma and choosing L0 = dom(E) ∪ FV(t1) (FV(t1) ∪ dom(E) ∪ {x}). We are left with the subgoal lets us complete the decidability proof.
The renaming lemma is simply a consequence of properties ∈ L. (E, y:T1 c t1 (substitution and weakening) that we have already proven about and conclude using typing rename.
the cofinite typing judgement. Importantly, showing these proper-ties does not require renaming. We can derive typing rename as follows. If x = y, then there is nothing to do. Otherwise, we rewritethe conclusion using subst intro as In general, then, developing metatheory in the locally namelessstyle involves the following steps.
1 c [x → fvar y] (t1 ) : T2 .
1. State definitions using exists-fresh quantification.
By the substitution lemma, typing subst, it suffices to show that 2. Restate the definitions using cofinite quantification.
1. E, y:T1 c fvar y : T1 and 3. Prove basic lemmas, such as subst intro.
4. Prove substitution and weakening lemmas.
5. Prove renaming lemmas.
9 Coq is a constructive logic, so a proof of this lemma is an algorithm thatproduces either a typing derivation, or a proof that one isn't possible.
6. Prove the equivalence of the cofinite and exists-fresh presenta- The simplicity of the example requires a slight change to the formaliza- tion of λ→, to annotate applications (app) with the argument type. This However, we can sometimes get by with even less. To begin with, change permits the proof to go through in the application case, but is other- observe that the exists-fresh definitions are needed only in the first wise independent of binding.
and last steps above. The main reason for stating the exists-fresh 11 The variable x must be fresh for L0 for the induction hypothesis to apply definitions is to check (informally) that the cofinite definitions ad- and must be fresh for dom(E) so that ok (E, x:T1). We also include equately encode the relations of interest. Thus, it is only necessary FV(t1) to maintain the invariant that terms are only opened with fresh to state the exists-fresh definitions for relations whose adequacy is crucial—those relations that appear hereditarily in the statements 12 While the freshness condition on y 6∈ dom(E) ensures that (E, y:T1) of theorems of interest. The style can be streamlined by omitting is well-formed, the freshness condition x 6∈ dom(E) could be derived withsome work from the second hypothesis; nevertheless we we choose to stickto a simpler and symmetric presentation.
13 The formal proofs can be found in file STLC Core Adequacy.v.
steps 1 and 6 for definitions of technical relations that are intro- which quantify bound variables over as many names as possible.
duced only to help with proofs, as long as the equivalence of the For example, they would state the typing rule for abstractions as existential and universal forms of definition is not actually needed in proofs (see Section 4.2).
∈ dom(E). (E, x:S a tx : T ) In fact, the style can be streamlined further, according to need and personal taste. One may (after gaining some familiarity) feel convinced that the cofinite definitions are adequate encodings of This form of quantification is natural, as there is no arbitrary choice one's informal ideas, without the need of a formal proof of equiva- of fresh name in rule A-TYPING-ABS, hence there is at most one lence with their "more obviously adequate" exists-fresh versions.14 derivation of a judgement E a t : T , and the associated in- In this case, steps 1 and 6 can be omitted. By doing this, one may duction principle is as strong as possible. The problem with rela- be risking adequacy of representation, but one is not risking con- tion a is that rule A-TYPING-ABS is too weak as an introduction sistency: the soundness of cofinite-quantified relations checked by rule, since it requires its premise to hold for every sufficiently fresh Coq is no more in question than the soundness of Coq itself.
name, where cofinite quantification (rule C-TYPING-ABS) allows a Finally, if we omit step 6, we can then prove renaming lemmas— finite number of problematic names to be excluded. In McKinna- step 5—only as needed, rather than going to the trouble of stating Pollack style one must prove the equivalence between and a and proving them for all relations. Indeed, as we described in Sec- (at significant cost in infrastructure) before metatheoretic results— tion 4.2, our experience has been that they are rarely needed.
step 4 in our style—can be developed, since is too weak in elim- In short, the core of our style is to define relations using cofinite ination and a is too weak in introduction for either to prove both quantification and to reason about those particular definitions, i.e., weakening and substitution lemmas for themselves. Thus our strat- steps 2 through 4. The remaining steps need not be carried out for egy for proving equivalence between definitions, which piggybacks every relation.
on standard metatheoretic results, fails in the McKinna-Pollackstyle.
Leroy's locally nameless solution to the POPLMARK Challenge As we mentioned in Section 2, we are not the first to propose a uses McKinna and Pollack's ideas. He takes universal definitions as locally nameless representation for languages with binders. Nev- the official ones, obtaining strong induction principles "for free", ertheless, our style of formal reasoning using this representation and does not explicitly define the exist-fresh definitions at all.
differs from previous work in important ways, requiring much less However, to make his proofs go through he needs to show that infrastructure as a result. In this subsection, we give a comparison exists-fresh forms are admissible for the universal forms. E.g., to the styles used by Gordon (1994), McKinna and Pollack (1993; Leroy proves the following lemma for his universally quantified 1999), and Leroy (2007). To obtain a meaningful comparison, we sometimes apply their styles to our definitions.
Gordon was the first to use a locally nameless representation ∈ FV(t) ⇒ E, x:T1 a tx : T2 ⇒ for formal reasoning about binders: he used them as a concrete E a abs t : T1 → T2.
datatype upon which to erect a type of named terms up to alphaequivalence. In contrast to our judgements (both the exists-fresh Such lemmas, which are essentially equivalent to showing that and cofinite versions), his are stated using the close operation in- and a define the same relation, must be stated and proved for every stead of open. For example, Gordon's local closure rule for abstrac- rule with binding in the development. The proof of such lemmas tion (in our notation) is: requires a significant amount of infrastructure related to renaming,so Leroy's style is a minor streamlining of the McKinna-Pollack Nominal Isabelle and Local Representation Gordon observed that the rule induction principle arising from thisform is "too weak" (Gordon 1994, Section 4) in that renaming a The nominal Isabelle package (Urban 2007; Urban et al. 2007a,b) variable with a fresh name is sometimes required. He derives a supports representation in Isabelle/HOL of languages with bind- strengthened induction principle by well-founded induction on the ing (as an extended notion of datatype) using a single species of length of a term (as is standard). Then, to avoid further reasoning name for both bound and free variables. Using the HOL type defi- about length, he uses this strengthened induction principle to derive nition facility, the package arranges that HOL equality of terms in another strengthened induction principle that picks a name fresh for these represented languages is up-to alpha equivalence, while users some finite set. However, Gordon's strengthened induction princi- need not define alpha equivalence or see any quotient structure. The ple is not the same as that arising from our form of cofinite quan- package supports multiple classes of names (e.g., type variables tification, since the induction hypothesis only applies to a single and term variables) in mutually inductive datatypes (e.g., terms and variable in the abstraction case. In this respect, Gordon's strength- dependent types) and multiple relations on them (e.g., typing and ened principle is more similar to that of Urban et al. (2007b) than to reduction). Using the Isabelle typeclass facility, the package au- ours. We get a stronger induction principle and stronger inversion tomatically provides definitions of name freshness and name per- principles automatically from the cofinite quantified forms.
mutation (renaming) polymorphic over these multiple aspects of a McKinna and Pollack (1993, 1999) proposed a style of develop- formalization. Importantly, given some syntactic restrictions on the ment for working with locally named terms. The most significant represented languages, the package automatically derives equivari- difference from our style is that it obtains strengthened induction ance lemmas and strengthened induction principles for formalized principles by stating universal definitions of inductive relations, languages. The nominal package involves no axiomatic extensionto Isabelle/HOL, hence is as safe as Isabelle/HOL itself. This nom- inal representation is a serious alternative to our style for users It is worth emphasizing that the exists-fresh versions are more obvi- ously adequate, in a technical sense: they can be formalized in a very weak who want to do formal metatheory. However it is based on a great theory—Primitive Recursive Arithmetic—while cofinite presentations in- deal of bespoke infrastructure only available in Isabelle/HOL, there volve rules with "infinitely many hypotheses" that cannot be formalized in are some syntactic restrictions, and certain aspects of formalization any conservative extension of PRA.
(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.
The heart of the POPLMARK Challenge is a proof of type sound- A locally nameless formalization (as we propose) or a locally ness of System F<:. This task was designed as a stress test for named formalization ( a la McKinna-Pollack) can be formalized formalized metatheory. Our solution closely follows the structure in many logics and proof tools, depending only on basic notions proposed in the appendix of the challenge's description.
like datatypes and inductively defined relations.15 In particular, To get a sense of how our solution compares to other solutions, the local representation can be seen as a nominal representation we measured the number of lemmas and steps of reasoning in- that doesn't happen to use any nominal binding; in this case the volved in several developments;16 the results are summarized in nominal relation of freshness of names for language structures Figure 5. Our study is restricted to Coq developments since there (terms, types, contexts, . . ) is the same as the local representation's are no meaningful metrics across different proof assistants. In this notion of non-occurrence. This leads to an interesting possibility: comparison, a step of reasoning is defined as the invocation of one local representations can be defined and reasoned about using the tactic, excluding trivial ones: intros (introduces hypotheses into nominal Isabelle package, getting the definitions of freshness and the context), auto (performs automated proof search), and simple renaming and the proofs of equivariance for free from the package.
variations of these two. We also exclude from the counts material Interestingly, the nominal package can also automatically infer a from libraries that are reusable across metatheory developments.
strengthened induction principle for inductive relations over local We isolate part 1A of the challenge (technical properties of the representations (with some syntactic restrictions); see (Urban and subtyping relation) from parts 1A+2A (preservation and progress) Pollack 2007) for more details.
because some submissions cover only part 1A.
A detailed comparison between nominal representation and lo- Even when attention is restricted to Coq developments, the com- cally nameless representation is beyond the scope of this paper, but, parison is necessarily rough, since the developments were carried as we are focusing on strengthened induction principles, we can out by different people with different preferences in the amount of remark that the locally nameless strengthened induction principle automation they used, etc. Nevertheless, a few interesting points (e.g., from rule C-TYPING-ABS or rule A-TYPING-ABS) is stronger emerge. The first line of the table shows that our style compares than the strengthened induction principle automatically derived by well against Vouillon's development, which uses pure de Bruijn the nominal Isabelle package. For a full explanation of the nom- indices—a representation commonly thought to be quite effective.
inal strengthened induction, see Urban et al. (2007b); here it is The solutions that do not use a standard de Bruijn or locally name- enough to observe that, when using such an induction principle, less representation (Stump and Hirschowitz & Maggesi) require one specifies not only the derivation being eliminated ("induction significantly more steps. The last line shows that our style re- on . . "), but also an arbitrary finitely supported structure to be used quires significantly less infrastructure than Leroy's solution, a lo- as a freshness context. Whenever a chosen name appears in an in- cally nameless solution faithful to McKinna and Pollack's way of duction hypothesis (e.g., the name that is bound in an abstraction dealing with the quantification of names. Chlipala's is a variation typing rule), that name is known to be fresh for the specified fresh- on an earlier version of Leroy's development and is the only one ness context. This solves many problems, as in the example above that is shorter than ours, mainly because Chlipala's proof script re- of weakening for the typing judgement. However, you must spec- lies heavily on development-specific tactics.
ify the freshness context when invoking induction. In contrast, the Although clever automation and development-specific tactics locally nameless strengthened induction principles, with their uni- can make scripts extremely small (Nipkow [2001] gives an impres- versally quantified fresh names, allow fresh instantiation of these sively automated proof of confluence, for example), they can also names later, at the point where you have seen the particular cases make them slow (hard to work with) and brittle (hard to reuse).
that must be proved. Since particular cases may involve existential Brittleness emerges when automation fails after some changes to quantifiers, you may not know what the necessary freshness context earlier definitions or lemmas: it can be hard to know exactly what is until after seeing a case and eliminating an existential quantifier.
has been broken and how to fix it. Of course, the other extreme of In such rare examples, the automatically derived nominal strength- no automation at all is also unmanageable, especially for metathe- ened induction principle is not adequate (a detailed hand proof is ory proofs, which involve many related arguments. Moreover, too necessary) while the locally nameless strengthened induction prin- little automation can also make scripts brittle: even a tiny change ciple works perfectly.
in definitions or statements of lemmas will require update. Aimingfor maximal robustness, our convention is to rely as much as pos-sible on automation for low-level details (e.g., proving that a term Practical Formal Metatheory is locally closed) while giving all the "important" arguments (theones that would appear in a rigorous paper proof) manually.
We close with a concrete discussion of our Coq realization of work-ing with cofinite quantification. We present the major developments Calculus of Constructions (CoC) we have carried out—System F<:, the Calculus of Constructions, This formalization contains three main components. The first is a and extensions of ML—to demonstrate that our techniques scale to proof of confluence for parallel beta-reduction. Its use of the vari- larger languages and are expressive enough for wide use. We dis- able closing operation requires slightly more advanced reasoning cuss issues specific to each development (e.g., dealing with multi- about binders. We have also used this development to evaluate our binders) as well as properties common to all of them (e.g., the con- scripts for robustness: we first completed a proof of confluence for ciseness and robustness on change of our scripts). Finally, we give the pure lambda calculus and then migrated it to CoC, preserving an overview of the structure of our developments for readers who the same flow of arguments and just adding the extra cases and up- may wish to use them as a basis for their own formalizations.
dating the names of some hypotheses.
The second part consists of a set of inversion results for the typing and the conversion judgments, which are quite technical 15 Some specialized tactics, as in the accompanying Coq code http:// in themselves but do not involve much difficulty with respect to arthur.chargueraud.org/research/2007/binders/, are useful, butnot essential. In any case these tactics are very much simpler than the 16 All are publicly available from http://alliance.seas.upenn.edu/ nominal Isabelle package.
Author (chronological order) Representation used Proof steps 1A+2A Hirschowitz & Maggesi de Bruijn (nested datatype) Figure 5. Comparison of Coq submissions to the POPLMARK Challenge Results formalized trusted definitions Preservation and progress Preservation and progress Preservation and progress Preservation and progress Figure 6. Complexity of our developments binders. This part is representative of the effort required for the substitution from one name to one term. Then, to prove subject re- CoC formalization: we felt that the largest share of the work was duction, for example, the substitution lemma is applied iteratively to understand and be able to state clearly the arguments involved.
in the cases involving multi-binders.
The fact that the proofs were machine-checked appeared to be onlya way to force oneself to understand all the details of the proofs Organization of Our Developments formalized, not as an extra burden to be dealt with.
The third and last part is the core of the preservation proof, Each of our developments is divided into three main parts: trusted which shares a significant amount of structure with the correspond- definitions, infrastructure, and core lemmas.
ing proof for System F The trusted definitions part contains the description of the lan- <: (only the steps of reasoning are more complex to follow). Compared to the System F guage formalized—the syntax of the language, its semantics, and <: development, the fact that terms and types are represented in a uniform way in CoC its type system, if any—and the statements of the main theorems and that proofs are more complex reduces the binding infrastructure which are to be proven about the language. This part is the only from about 60% of the total development down to 35% percent.
material that needs to be trusted, in the following sense: if one is Compared to Barras's formalization of CoC in Coq (1997) using convinced about the adequacy of these definitions and trusts that a pure de Bruijn representation, our style saves us from numerous Coq correctly type-checks all proofs in the development, then one issues associated with shifting indices—particularly bothersome can have confidence that the system has been formally certified.
when working with CoC's dependent types—and so, unlike Barras, The infrastructure part sets up the machinery required for the we did not need clever engineering of the statements of lemmas to core lemmas and consists of several components: make them fit the representation used.
1. Language-specific specializations of tactics for working with cofinite quantification, e.g., to automatically choose a set L when applying a rule that uses cofinite quantification.
We also investigated how to extend the basic λ→ development with 2. Proofs about properties of substitution (Figure 2).
features such as datatypes, fixpoints, references, exceptions, pattern 3. Proofs that local closure is preserved by various operations, e.g., matching, and ML-style polymorphic types. Then, building on the substitution (Section 3.3).
individual successes of each of these extensions, we set up the for-malization of a language containing all of these features together.
4. Regularity lemmas which state that relations contain only lo- This experiment demonstrates that our style can be applied to full- cally closed terms (Section 3.3).
featured programming languages, not just tiny lambda-calculi.
5. Hints to enable Coq's automation to use regularity lemmas.
Pleasingly, most of the arguments that would be omitted as "trivial" on paper and which do not involve binders are solved by Note that the lemmas about substitution are similar from one lan- the auto tactic. In particular, the infrastructure lemmas do not need guage to the next. When setting up a new development, those who any change when we add features like pairs or references. The key wish to get to "interesting" proofs quickly may state as axioms proofs—preservation and progress—contain respectively in 60 and properties of substitution and regularity lemmas, proving them only 80 lines, which seems reasonable for a system with 24 typing rules.
after they believe that their main proofs will go through. In this A key idea involved in this development is a treatment of multi- manner, one can "test-drive" a language definition without having binders, used to encode ML type schemes, patterns, and recur- to revise infrastructure proofs as the definition is modified.
sion. The basic operation on a multi-binder is to open it with a Finally, the core lemmas part contains the lemmas that would list of terms. A bound variable pointing to the jth variable bound normally be stated in an informal presentation. The statements by the ith binder above the current position is represented as closely match their informal counterparts, and the proofs contain (trm bvar i j). Free variables are still represented as one single few uninteresting details—facts about local closure and freshness name and substitution lemmas are still stated in terms of an atomic side conditions are almost always handled automatically.
We conclude this section with a breakdown of our developments by the number of definitions and lemmas in each part, as well as the Thorsten Altenkirch. A formalization of the strong normalization proof for number of proof steps required to prove the lemmas; the results are System F in LEGO. In Bezem and Groote (1993), pages 13–28.
summarized in Figure 6. The number of trusted definitions gives Andrew W. Appel. Foundational proof-carrying code. In IEEE Symposium an idea of the size of the language formalized. The number of core on Logic in Computer Science (LICS), Boston, Massachusetts, pages lemmas gives an idea of the theoretical complexity of the develop- 247–258, June 2001.
ment; recall that these lemmas correspond closely with results thatwould be proven informally. The amount of infrastructure, in terms Michael Ashley-Rollman, Karl Crary, and Robert Harper. Submission to the POPLMARK challenge. Available from http://www.cis.upenn.
of both lemmas and steps, is proportional to the number of binding constructs and relations in the language. A comparison between plclub/mmm/, 2005.
figures from the last two columns suggests that the amount of in- Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, frastructure work is reasonable compared to the core proof work— Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Wash-burn, Stephanie Weirich, and Steve Zdancewic. Mechanized metathe- especially since infrastructure proofs follow a standard pattern and ory for the masses: The POPLMARK challenge. In Joe Hurd and Tom are easily set up. More precisely, the ratio "infrastructure over core Melham, editors, Theorem Proving in Higher Order Logics: 18th Inter- proofs" increases with the number of binding constructs involved national Conference, TPHOLs 2005, volume 3603 of Lecture Notes in but decreases with the inherent complexity of the development.
Computer Science, pages 50–65. Springer, 2005.
Henk P. Barendregt. The Lambda Calculus. North Holland, revised edition, We have argued for a novel style for formalizing programming- Bruno Barras and Benjamin Werner. Coq in coq. Available from http: language metatheory, based on a combination of locally nameless representation with a cofinite idiom for quantifying free names in M. Bezem and J. F. Groote, editors. Typed Lambda Calculi and Applica- tions: International Conference on Typed Lambda Calculi and Appli- This design satisfies the evaluation criteria of POPLMARK.
cations, TLCA '93, volume 664 of Lecture Notes in Computer Science, First, our presentation is transparent: the proofs closely follow their 1993. Springer.
informal equivalents. Second the overheads of the approach are Anna Bucalo, Furio Honsell, Marino Miculan, Ivan Scagnetto, and Martin low: we do not need manual proofs of freshness side-conditions nor Hoffman. Consistency of the theory of contexts. J. Funct. Program, 16 reasoning about alpha-equivalence, and only on rare occasions do we need to justify well-formedness of objects (e.g. local closure) Adam Chlipala.
Submission to the POPLMARK challenge, part or explicitly rename variables. When we do, the required proofs Available from http://www.cs.berkeley.edu/ adamc/ of renaming lemmas follow with virtually no infrastructure. At the poplmark/, 2006.
same time, there is no need for external tools, and the style works in The Coq Development Team. The Coq proof assistant reference manual, any general purpose theorem prover (although we found Coq to be version 8.1. Available from http://coq.inria.fr/, 2007.
well-suited to the task). In our scripts, definitions and results about Thierry Coquand. An algorithm for testing conversion in type theory. In variables, freshness, and environments are factored into a reusable G´erard Huet and Gordon Plotkin, editors, Logical Frameworks, pages library. Finally, experience with a number of large developments 255–279. Cambridge University Press, 1991.
suggests that the approach is "complete" in the informal sense thatany language definition and accompanying reasoning techniques Karl Crary. Toward a foundational typed assembly language. In POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on that would be accepted as informally correct can be carried out in Principles of Programming Languages, pages 198–212. ACM Press, this style. Our formalizations provide a good starting point for new work—reports from early adopters confirm that modifying them ismuch easier than starting a new development from scratch.
N. G. de Bruijn.
Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church- In the future, we would like to integrate our approach with the Rosser theorem. Indagationes Mathematicae, 34(5):381–392, 1972.
Ott tool (Sewell et al. 2007), which automatically generates Coq(and LAT Jo¨elle Despeyroux, Amy Felty, and Andr´e Hirschowitz. Higher-order ab- EX) definitions from compact, high-level language descrip- tions. A more ambitious next step is to study the possibility of auto- stract syntax in Coq. In Typed Lambda Calculi and Applications, SecondInternational Conference on Typed Lambda Calculi and Applications, matically generating the required infrastructure proofs, which fol- TLCA '95, volume 902 of Lecture Notes in Computer Science, pages low a fairly simple pattern. Finally, we would like to explore cer- 124–138. Springer, 1995. Also available as INRIA Research Report tified programming of tools such as type checkers and compilers that must deal with binders. In the long term, we hope that our Peter Dybjer. Inductive families. Formal Aspects of Computing, 6:1–26, techniques will help with the verification of both specifications and implementations of programming languages.
Jonathan M. Ford and Ian A. Mason. Operational techniques in PVS — Many thanks to the members of the Penn A preliminary evaluation. Electronic Notes in Theoretical Computer PLClub for extensive feedback and discussion, and to Michael Science, 42, 2001.
Norrish and Christian Urban for important technical insights and Gerhard Gentzen.
The Collected Papers of Gerhard Gentzen.
to the POPL reviewers, Bob Harper, Peter Sewell, and Karl Crary Holland, 1969. Edited by Mandred Szabo.
for helping improve the final version. This work was supported Andrew D. Gordon. A mechanisation of name-carrying syntax up to alpha- by NSF grant 545886, CRI: Machine Assistance for Program- conversion. In J. J. Joyce and C.-J. H. Seger, editors, Higher-order Logic ming Language Research. Pollack thanks the International Centre Theorem Proving And Its Applications, Proceedings, 1993, volume 780 for Mathematical Sciences (Edinburgh) Workshop on Abstraction, of Lecture Notes in Computer Science, pages 414–426. Springer, 1994.
Substitution and Naming and the EU Framework 6 Coordination Andrew D. Gordon and Tom Melham. Five axioms of alpha-conversion.
Action 510996, TYPES.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Provingin Higher Order Logics: 9th International Conference, TPHOLs '96,volume 1125 of Lecture Notes in Computer Science, pages 173–190.
Springer, 1996.
Robert Harper and Daniel R. Licata. Mechanizing metatheory in a logical gramming Language Design and Implementation, pages 199–208. ACM Journal of Functional Programming, 17(4–5):613–673, Press, 1988.
Frank Pfenning and Carsten Sch¨urmann. System description: Twelf — A Robert Harper, Furio Honsell, and Gordon Plotkin.
meta-logical framework for deductive systems. In Harald Ganzinger, defining logics. Journal of the ACM, 40(1):143–184, 1993.
editor, Automated Deduction, CADE 16: 16th International Conferenceon Automated Deduction, volume 1632 of Lecture Notes in Artificial Dimitri Hendriks and Vincent van Oostrom. Adbmal. In F. Baader, editor, Intelligence, pages 202–206. Springer, 1999.
Automated Deduction – CADE-19, volume 2741 of Lecture Notes inArtificial Intelligence, pages 136–150. Springer–Verlag, 2003.
Andrew M. Pitts. Nominal logic, a first order theory of names and binding.
Information and Computation, 186:165–193, 2003.
Peter Homeier.
A proof of the Church-Rosser theorem for the lambda calculus in higher order logic.
In Richard J. Boulton and Paul B.
Randy Pollack.
Reasoning about languages with binding: Can we do Jackson, editors, TPHOLs 2001: Supplemental Proceedings, pages 207– it yet?, February 2006. Presentation, slides available from http:// 222. Division of Informatics, University of Edinburgh, September 2001.
Available as Informatics Research Report EDI-INF-RR-0046.
Robert Pollack. Closure under alpha-conversion. In H. Barendregt and Furio Honsell, Marino Miculan, and Ivan Scagnetto. The theory of contexts T. Nipkow, editors, TYPES'93: Workshop on Types for Proofs and Pro- for first order and higher order abstract syntax.
Electronic Notes in grams, Nijmegen, May 1993, Selected Papers, volume 806 of Lecture Theoretical Computer Science, 62, 2002.
Notes in Computer Science, pages 313–332. Springer, 1994a.
G´erard Huet. The constructive engine. In Raghavan Narasimhan, editor, Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended A Perspective in Theoretical Computer Science: Commerative Volume Calculus of Constructions. PhD thesis, Univ. of Edinburgh, 1994b.
for Gift Siromoney. World Scientific Publishing, 1989. Also available as Dag Prawitz. Natural Deduction: Proof Theoretical Study. Almquist and INRIA Technical Report 110.
Wiksell, Stockholm, 1965.
G´erard Huet. Residual theory in λ-calculus: A formal development. Journal Ole Rasmussen. The Church-Rosser theorem in Isabelle: A proof porting of Functional Programming, 4(3):371–394, July 1994. Also available as experiment. Technical Report 364, University of Cambridge, Computer INRIA Research Report 2009 (August 1993).
Laboratory, March 1995.
Gerwin Klein and Tobias Nipkow. A machine-checked model for a Java- Wilmer Ricciotti. Submission to the POPLMARK challenge, part 1a. Avail- like language, virtual machine, and compiler. ACM Transactions on able from http://ricciott.web.cs.unibo.it/, 2007.
Programming Languages and Systems, 28(4):619–695, 2006.
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, J. L. Krivine. Lambda-Calculus, Types and Models. Ellis Horwood, 1990.
Thomas Ridge, Susmit Sarkar, and Rok Strniˇsa. Ott: Effective tool sup- Daniel K. Lee, Karl Crary, and Robert Harper. Towards a mechanized port for the working semanticist. In ICFP '07: Proceedings of the 2007 metatheory of Standard ML. In POPL '07: Proceedings of the 34th ACM SIGPLAN International Conference on Functional Programming, Annual ACM SIGPLAN-SIGACT Symposium on Principles of Program- pages 1–12. ACM, 2007.
ming Languages, pages 173–184. ACM Press, 2007.
Natarajan Shankar. A mechanical proof of the Church-Rosser theorem.
Xavier Leroy. Formal certification of a compiler back-end, or: programming Journal of the Association for Computing Machinery, 35(3):475–522, a compiler with a proof assistant. In Proc. of the 33rd Symposium on Principles of Programming Languages, pages 42–54. ACM Press, 2006.
Allen Stoughton. Substitution revisited. Theoretical Computer Science, 59 Xavier Leroy. A locally nameless solution to the POPLmark challenge.
Research report 6098, INRIA, January 2007.
Christian Urban. Nominal techniques in Isabelle/HOL. Journal of Auto- Zhaohui Luo and Robert Pollack. The LEGO proof development system: matic Reasoning, 2007. To appear; available from http://www4.in.
A user's manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, May 1992.
Christian Urban and Randy Pollack.
Locally nameless representation Conor McBride and James McKinna. Functional pearl: I am not a number— in Nominal Isabelle. Talk at Workshop on Mechanizing Metatheory.
I am a free variable. In Haskell '04: Proceedings of the 2004 ACM Available from www4.in.tum.de/ urbanc/Publications/ln.pdf, SIGPLAN Workshop on Haskell, pages 1–9. ACM Press, 2004.
James McKinna and Robert Pollack. Pure Type Systems formalized. In Christian Urban, Stefan Berghofer, and Julien Narboux. Nominal datatype Bezem and Groote (1993), pages 289–305.
package for Isabelle/HOL.
Available from http://isabelle.in.
James McKinna and Robert Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning, 23(3–4):373–409, 1999.
Christian Urban, Stefan Berghofer, and Michael Norrish.
variable convention in rule inductions.
In Proceedings of the 21th Tobias Nipkow. More Church-Rosser proofs (in Isabelle/HOL). Journal of Conference on Automated Deduction (CADE 2007), volume 4603 of Automated Reasoning, 26(1):51–66, January 2001.
Lecture Notes in Computer Science, pages 35–50. Springer, 2007b.
Michael Norrish and Konrad Slind. HOL 4. Available from http://hol.
Ren´e Vestergaard and James Brotherston. A formalised first-order conflu- ence proof for the λ-calculus using one-sorted variable names. Informa- Frank Pfenning and Conal Elliot. Higher-order abstract syntax. In PLDI tion and Computation, 183(2):212–244, 2003.
'88: Proceedings of the ACM SIGPLAN 1988 Conference on Pro-

Source: http://rnyingma.synrc.com/publications/cat/Type%20and%20Effect/binders.pdf