A formalization of a concurrent object calculus up to α-conversion

Guillaume Gillard

INRIA Sophia Antipolis

Abstract. We experiment a method for representing a concurrent object calculus in the Calculus of Inductive Constructions. Terms are first defined in de Bruijn style, then names are re-introduced in binders. The terms of the calculus are formalized in the mechanized logic by suitable subsets of the de Bruijn terms; namely those whose de Bruijn indices are relayed beyond the scene. The α-equivalence relation is the Leibnitz equality and the substitution functions can de defined as sets of partial rewriting rules on these terms. We prove induction schemes for both the terms and some properties of the calculus which internalize the renaming of bound variables . We show that, despite that the terms which formalize the calculus are not generated by a last fixed point relation, we can prove the desire inversion lemmas. We formalize the computational part of the semantic and a simple type system of the calculus. Finally , we prove a subject reduction theorem and see that the specifications and proofs have the nice feature of not mixing de Bruijn technical manipulations with real proofs.

1 Introduction

Providing a satisfactory method to encode the binding operators of a programming language when we want to formalize it in a Logical Framework is still a challenge. Although many different methods have been proposed so far, none seems completely satisfactory. From de Bruijn codes to higher order encoding each method has is advantages and disadvantages, its supporters and its detractors. A major problem raised by all these methods is that theorems and theirs proofs become highly linked with chosen encoding. In other words, if it is sometimes possible to have specifications and theorems close to the unmechanized version (which is not the case for de Bruijn encoding), the proof structures are themselves very different from the informal ones. In this paper, we show that the method proposed in [Gor94] for representing binders in mechanized logic can successfully be extended to a large calculus with different kinds of binders. Beside, we show that, once some work has been done with de Bruijn indices, real proofs do not manipulate them moreover, they are similar to the unmechanized ones.

We have chosen to formalize the concς-calculus [GH98], a concurrent object calculus consisting of M. Abadi and L. Cardelli’s imperative object calculus impς [AC96] extended with primitives from the π-calculus [MPW92]. This calculus was introduced as a possible formalism for modeling computations based on concurrent processes and objects. We think that formal proofs of properties of protocols can be realized within proof-assistant if we have good methods for encoding such calculus. Our choice of this calculus is motivated by its size, its different kinds of binder and its good expressiveness, thus giving an idea of the real problems that arise when we encode such formalisms in computational logics.

The COQ system we use for our implementation is a proof-assistant based on the calculus of inductive constructions [Wer94], a higher order logic with dependent types and inductive definitions. All the proofs have been done with the user-interface CtCoq [BBC^{+}97]. This paper has been written so as to be understood by people not familiar with the COQ system. We use mathematical notations instead of the COQ syntax and we only show significant parts of large COQ encodings. Please refer to [Gil00] for a full presentation of our technical results.

Organization of the paper: In section 2 we formalize the concς-calculus in COQ. In section 3 we prove a more powerful induction theorem for the terms of the calculus which internalizes the renaming of bound names. In section 4 we formalize the semantics of the concς-calculus in COQ and we produce an efficient induction principle for the semantic relation. In section 5 we give a simple type system for the calculus and discuss the problems raised by the inversion lemmas generated by the COQ system on this example. Section 6 presents the statement and the proof of the subject reduction theorem. Section 7 is a short discussion about the formalizing technique we used. Finally, section 8 draws some conclusions.

2 The concς-calculus

This calculus was first introduced by A. Gordon and P. Hankin. It is the imperative object calculus impς of M. Abadi and L. Cardelli in which objects are located at addresses, extended with a parallel composition and the name restriction operator from the π-calculus. The reader interested in a more detailed presentation of this calculus should refer to [GH98].

2.1 Informal syntax of the calculus

We assume that there are infinite disjoint sets of references, variables and labels. We distinguish references, representing addresses of stored object (channels in the π-calculus) from variables, representing intermediate values (variables in the λ-calculus). Let us call both notions names. The expressions of the language are defined as follows:

In the method ς(x)b, and in the expression let x = a in b the variable x is bound in b. In a restriction, (νp).a the reference p is bound in a. The notation a = b means that the terms a and b are equal up to bound names renaming and reordering of the labeled components of objects.

Table 1. Syntax of the informal concς-calculus

l  labels
u,v::=  result
x,y,z  variables
p,q  references
a,b,c::=  terms
u,v  result
p ↦ d  denomination
p.l  method select
p.l ⇐ ς(x).b  method update
clone(p)  cloning
let x = a in b  let
a ↱ b  parallel composition
νp.a  restriction
d::=  denotations
[l_{i} = ς(x_{i})a_{i} ^{i∈1..n}] object

2.2 de Bruijn specification

We define a de Bruijn syntax (table 2) in which free names n, m are encoded by named names (reference?). Variables x,y,z are either free variables x,y,z or de Bruijn variables (dvar i), (dvar j), labels l,l_{i} are named and references p,q are either free references p,q or de Bruijn references (dref i),(dref j). We assume there are infinite disjoint sets of references, variables and labels and that equality is decidable on each of these sets.

Table 2. de Bruijn formalism

DB =^{def} x | p | p ↦ ODB | DB.l |

DB.l ⇐_{db} DB | clone(DB) | let_{db} DB in DB | DB ↱ DB | ν_{db}.DB

ODB =^{def} [] | [l : DB :: ODB]_{db}

Except otherwise stated in the sequel of the paper we no longer refer to references, variables, labels, results of the informal calculus described in 2.1. De Bruijn terms (DB) a,b,c are called dbterm, lists of dbterms (ODB) are called denotation and for readability reasons, var and ref will be use for free variables and free references respectively in all our formal definitions.

The binding constructors here are ⇐_{db}, let_{db} (in their second argument) and the object-constructor (the self variable of each method is bound by [ ]_{db}) for de Bruijn variables. The ν_{db} operator is the only binding constructor for de Bruijn references. Objects are represented by lists. Although sets seem closer to the idea of objects (a collection of attributes and methods), we cannot define object as sets because sets in COQ are specified as predicates, and predicates cannot be used in the type of a constructor of an inductive set. Moreover, COQ provides an efficient tool for generating induction scheme for mutual inductive definitions when some type is a list of another ^{1}.

Our syntax is a bit more general than the one proposed by A. Gordon for his concς-calculus in the sense that we allow cloning, method calling, and method updating not only for results but for all terms of our syntax. This choice was motivated because dbterm are less nested than they would have been with a de Bruijn result type. Since the concς-calculus terms will eventually be identified by an inductively defined subset of dbterm this will not have any consequences on its formalization in COQ.

Thanks to de Bruijn indices we do not need an alpha-equivalence notion and a = b means that the dbterm a and b are equal in the sense of the Leibnitz equality. De Bruijn formalization for binders takes off the syntax its intuitive meaning. We shall show how to recover it later on (see 2.5).

As we have de Bruijn indices for both references and variables, we define two degree functions (computing the usual notion of degree for a term with de Bruijn indices [dB94]), one for each kind. We omit their formal definitions here so that readers do not get confuse with to many technical details (see [Gil00] for more details). We generalise the notion of closed de Bruijn terms to our calculus such that a dbterm is said to be closed when both its degrees are zero.

2.3 Function as binders

Abstraction and instantiation functions. We define a variable abstraction function Abst_{v}. For a given dbterm a, Abst_{v}(a i x) is computed by substituting in a all the occurrences of the variable x by the de Bruijn variable (dvar i). The substitution is defined recursively on the dbterms such that the Bruijn indices substituted is increased by one each time a binder is met. In a dual way, we define an instantiation function Inst_{v}. Inst_{v}(a i x) is computed by substituting all the occurrences of (dvar i) in a by the variable x. Similarly, we define Abst_{r} and Inst_{r} on references.

Functions as constructors We define new functions on dbterms let, res, and sigma behaving like the de Bruijn binding operators except that they use names in their arguments (see table 3). In the following, we shall write let x := a in b for (let x a b), νp.a for (res p a) and ς(x).a for (sigma x a). We will also drop the _{db} mark in a constructor when it can be guessed from the context.

2.4 Substitution and α-equivalence

To relegate de Bruijn indices of the underlying terms behind the scene we also need to define two new substitution functions Subst_{v} and Subst_{r}. Intuitively

1 Using the Scheme tactic

Table 3. Functions as constructor

\begin{matrix}(res p a) =^{def} ν_{db}.Abst_{r}(a 0 p) & (sigma x a) =^{def} Abst_{v}(a 0 x) \\ (let x a b) =^{def} let_{db} a in Abst_{v}(a 0 x) \end{matrix}

these functions are defined to rename free names in dbterms. Their definitions (see definition table 4) use de Bruijn indices in their bodies but, with some work, we shall manipulate them without referring to de Bruijn indices (see 3.2). We write a[x/y]_{v} and a[p/q]_{r} for Subst_{v}(a y x) and Subst_{r}(a q p) respectively.

Table 4. Substitution functions

Subst_{v}(a x y) =^{def} Inst_{v}(Abst_{v}(a 0 x) 0 y)  Subst_{r}(a q p) =^{def} Inst_{r}(Abst_{r}(a 0 q) 0 p)

If we think of the ν, let and ς function as constructors and Subst_{v} and Subst_{r} as renaming functions, we prove that α-equivalent dbterms are encoded in our formalism by a unique dbterm.

2.5 Formalization of the syntax

The result type (u,v,) is defined as the disjoint union of our free names:

result =^{def} var | ref

The inductive predicate Term (table 5) defines the subset of dbterm which formalizes the concς-calculus. The proof of correctness of this encoding is straightforward (omitted) if one thinks of let, res and sigma as constructors.

From now on, we shall call Term, a dbterm having the Term property and write ∀a : T erm.(P a) as a short hand for ∀a : dbterm.(T erm a) ⇒ (P a) in the translation of our COQ notations. Terms are based on a de Bruijn formalism but de Bruijn indices are hidden in the syntax by the let, res and sigma functions.

3 An induction principle for the concς-calculus

In the sequel, for readability reasons, we only show one (significant) case of the theorems. A more detailed presentation is available in [Gil00].

Table 5. formalization of the concς-calculus in COQ

T erm : dbterm → P rop :=

Resu: ∀r : result.(T erm r)
| Deno: ∀p : ref.∀obj : denotation. (OT erm obj) ⇒ (T erm p ↦ obj)
| Msel: ∀l : labels.∀u : result. (T erm u.l)
| Mupd: ∀u : result.∀a : dbterm.∀l : labels.∀x : var.
(T erm a) ⇒ (T erm u.l ⇐ ς(x).a)
| Clone: ∀u : result.(T erm (clone u))
| Let: ∀a, b : dbterm.∀x : var.(T erm a) ⇒ (T erm b) ⇒ (T erm let x := a in b)
| Par: ∀a, b : dbterm.(T erm a) ⇒ (T erm b) ⇒ (T erm a ↱ b)
| Res: ∀a : dbterm.∀p : ref. (T erm a) ⇒ (T erm νp.a)

with OT erm : denotation → P rop :=

Mnul:  (OT erm [])
| Mocons: ∀l : label.∀a : dbterm.∀obj : denotation.∀x : var.
(T erm a) ⇒ (OT erm obj) ⇒ (OT erm (l : ς(x).a :: obj))

3.1 The induction scheme generated by the COQ system

It appears that the induction scheme generated by COQ (table 6) for the predicate Term is not powerful enough for our purpose^{2} .

Table 6. Induction scheme generated by COQ

Term_ind:= ∀P : dbterm → P rop.

⋯ ⟨∀x : var.∀a, b : T erm.(P a) ⇒ (P b) ⇒ (P let x := a in b)⟩ ⇒ ⋯

∀a, b : T erm.(P a b).

For example, it is not clear how one can derive the fact that Terms are closed under the substitution Subst_{v} and Subst_{r} with it. We shall not be able to deduce (T erm (let x := a in b)[z/y]_{v}) from (T erm a[z/y]_{v}) and (T erm b[z/y]_{v}) because we have not the necessary informations on x, y and z to compute (let x := a in b)[z/y]_{v}. In this COQ formalization of the concς-calculus α-equivalence terms are equal. We want to integrate inside the induction scheme of Term the fact that bound names, in Terms, can always be renamed .

2 Actually we need to use the Scheme tactic to generate an efficient principle

3.2 An intermediate induction scheme for Terms

We define a new function length on dbterms which computes the numbers of constructors appearing in a term. The order ≤_{length} induced on dbterms by this function is well founded and we show that renaming names in a dbterm does not change its length. Using the general induction theorem for well founded relation with respect to ≤_{length} we prove a more powerful induction scheme than Term_ind for the Term relation (table 7).

Table 7. Intermediate induction scheme

Term_length_ind:= ∀P : dbterm → P rop.

⋯

∀x : var.∀a, b : T erm.(P a) ⇒ ⟨∀b′ : T erm. length(b) = length(b′) ⇒ (P b′)⟩ ⇒

(P let x := a in b)⟩ ⇒

⋯ ∀a, b : T erm.(P a b).

With this theorem, as the length of dbterms is invariant for the renaming functions, we prove that substitution can be propagated inside binders for Terms if the side conditions are satisfied (see table 8).

Table 8. substitution rewriting rules for the let binder

let_rw1: ∀x, y, z : var.∀a, b : T erm.x ≠ y ⇒ x ≠ z ⇒

(let x := a in b)[z/y] = let x := a[z/y] in b[z/y].

let_rw2: ∀x, y : var.∀a, b : T erm.(let x := a in b)[y/x] = let x := a[y/x] in b.

3.3 The full induction scheme for Terms

The use of the length function inside Term_length_ind is not satisfactory because this is not natural. We prove a final induction scheme on Term (table 9) using the Term_length_ind theorem and the properties of the substitutions functions we have deduced from it.

This induction scheme internalizes the property that bound names can always be chosen outside any set of names in the context.

Example: Given a property P on T erm, we prove that it holds for all T erms using the term-induction theorem. In order to prove that (P let x := a in b) holds, we select a finite set X and try to solve our goal under the assumptions (P a), (P b) and x ∉ X. Giving the set X amounts to specify that x is a fresh variable.

Table 9. Induction scheme for the Term predicate

Term_induction:= ∀P : dbterm → P rop.

⋯ (∀a : T erm.(P a) ⇒ ⟨∃X : set.(F inite X)∧

∀x : var.∀b : T erm. x ∉ X ⇒ (P b) ⇒ (P let x := a in b)⟩) ⇒ ⋯

∀a, b : T erm.(P a b).

4 Semantics of the concς-calculus

The semantics of the calculus is given by a reduction relation and a structural congruence. The formalization of the reduction rules in COQ is natural and we can prove an induction scheme which internalizes α-renaming .

4.1 Rules for the semantics

Informal semantics. Terms of the calculus are interpreted either as processes or as expressions. Expressions and processes are concurrent computations but an expression is expected to return a result while a process is not. As opposed to many concurrent calculi the parallel composition (↱) is not commutative. The term a ↱ b is an expression in which a and b run in parallel. Its result is the result returned by b; any result returned by a is discarded. The structural congruence (≡), except from the unusual behavior for (↱) is standard. The reduction relation (→_{red}) (table 10) is the matching piece to the β-reduction for the λ-calculus. The structural congruence relation allows the rearrangement inside a term so that reduction may be applied. Please refer to [GH98] for the motivations and more details on this semantics.

Table 10. Reduction relation: a → b

For the first three rules, let d = [l_{i} = ς(x_{i})b_{i}^{i∈1..n}].

(p ↦ d) ↱ p.l_{j} → (p ↦ d) ↱ b_{j}[p/x_{j}]  if j ∈ 1..n
(p ↦ d) ↱ (p.l_{j} ⇐ ς(x).b) → (p ↦ d′) ↱ p  if j ∈ 1..n
d′ = [l_{j} : ς(x).b, l_{i} = ς(x_{i})b_{i} ^{i∈(1..n)−j}]
(p ↦ d) ↱ (clone p) → (p ↦ d) ↱ νq.((q ↦ d) ↱ q) if q ∉ fn(d)
let x := p in a → a[p/x]
νp.a → νp.a′  if a → a′
(a ↱ b) → (a′ ↱ b)  if a → a′
(b ↱ a) → (b ↱ a′)  if a → a′
let x := a in b → let x := a′ in b  if a → a′
a → b  if a ≡ a′, b ≡ b′, a′ → b′

The notations fn(a) and fv(a) denote respectively the sets of free names and free variables in the expression a. The expression a[p/x] is the notation for the substitution of the reference p for each free occurrence of the variable x in the expression a.

Formalization in COQ. We use two inductive definitions to formalize the above relation in COQ. The first one (table 11) is a restriction to effective reductions in terms. The second one (table 12) is the complete formalization in the COQ system of the semantics (proof omitted here). We use this trick to prevent looping in the proofs. In the sequel of this paper we shall focus on the first definition.

The COQ formalizations of both relations are the natural translations of the rules in table 10 into inductive definitions (→_{red} and →_{eval}). The →_{red} relation is defined for Terms and not dbterms so, for every dbterm a appearing in the COQ definition of →_{red} (T erm a) must hold.

Table 11. Formalization of the →_{red} relation in COQ

→_{red}: dbterms → dbterms → P rop :=

⋯

Let_red1: ∀a : T erm.∀p : ref.(let x := p in a) →_{red} a[p/x]_{∗}

⋯

For any given term a, Subst_{∗}(a x p), written a[p/x]_{∗}, is computed by substituting all the occurrences of the variable x by the reference p in a. In the COQ system, Subst_{∗} must be defined on dbterms and de Bruijn indices are used in the body of this function. With the help of technical lemmas, we show that Subst_{∗} restricted to Terms can be manipulated without dealing with de Bruijn indices.

Table 12. Formalization of the reduction relation →_{eval} in COQ

\begin{matrix}→_{eval}: dbterm → dbterm → P rop := \\ Eval: & ∀a, a′, b, b,: T erm.(a ≡ a′) ⇒ (b ≡ b′) ⇒ (a′ →_{red} b′) ⇒ (a →_{eval} b) \end{matrix}

4.2 Induction scheme for the semantics

As before, for readability reasons, we only show one (significant) part of the theorems. Courageous readers could refer to [Gil00] for a more detailed presentation.

We can extend the induction scheme for the →_{red} relation as we did for the Term predicate. In the induction scheme generated by the COQ system (table 13) we do not have any informations for binded names.

Table 13. →_{red} induction scheme generated by COQ

Red_ind:= ∀P : dbterm → dbterm → P rop.

⋯

(∀p : ref.∀a, b : T erm.(a →_{red} b) ⇒ (P a b) ⇒ (P νp.a νp.b)) ⇒ ⋯

∀a, b : dbterm.(a →_{red} b) ⇒ (P a b).

Following the idea of the section 3 we can produce an extended induction scheme which internalizes the α-renaming of bound names in proofs. By using the general well founded induction theorem for a suitable order on pairs of dbterm we prove an intermediate theorem (table 14) in which the length of dbterm is introduced.

Table 14. →_{red} induction scheme with the length function

Red_length_ind:= ∀P : dbterm → dbterm → P rop.

⋯ (∀p : ref.∀a, b : T erm. ⟨∀a′, b′ : T erm. length(a) = length(a′) ⇒ length(b) = length(b′) ⇒ (a′ →_{red} b′) ⇒ (P a′ b′)⟩

⇒ (a →_{red} b) ⇒ (P νp.a νp.b)) ⇒ ⋯

∀a, b : dbterm.(a →_{red} b) ⇒ (P a b).

Finally , we prove the induction scheme (table 15) in which bound names can be chosen outside the set of names in the context. To prove the theorem, we first need an intermediary lemma stating that →_{red} is closed for names renaming. More precisely, we show that →_{red} is closed for names renaming provided that names are renamed in new names.

Table 15. →_{red} induction scheme

Red_induction:= ∀P : dbterm → dbterm → P rop.

⋯ ⟨∃Q : set.(F inite Q) ∧

(∀p : ref.∀a, b : T erm.p ∉ Q ⇒ (a →_{red} b) ⇒ (P a b) ⇒ (P νp.a νp.b))⟩ ⇒ ⋯

∀a, b : dbterm.(a →_{red} b) ⇒ (P a b).

5 Well-formed terms

The concς-calculus can be typed to distinguish expressions from processes. This very basic types system has only two types Exp and P roc standing for expressions and processes respectively. Basically, this typing system only ensures that proper processes cannot appear in a context expecting an expression and that references are correctly handled in a term. A term a is defined as an expression or a process if a : Exp and a : P roc, respectively.

5.1 Definition

The typing rules are define in table 16. T stands for either Exp or P roc. The domain of a term a, dom(a) is the set of the free references representing the addresses of an object. Please refer to [GH98] for a general overview.

Table 16. The well − formed relation

(Well Result) (Well Clone)  (Well Res)
\overline{u : Exp}  \overline{clone(u) : Exp} \frac{a : T p ∈ dom(a)}{νp.a : T}
(Well Select) (Well Concur) (Well Update)
\overline{u.l : Exp}  \frac{a : Exp}{a : P roc}  \frac{b : Exp dom(b) = ∅}{u.l ⇐ ς(x)b : Exp}
(Well Let)  (Well Par)
\frac{a : Exp b : Exp dom(b) = ∅}{let x := a in b : Exp} \frac{a : P roc b : T dom(a) ∩ dom(b) = ∅}{a ↱ b : T}

(Well Object)

\frac{b_{i} : Exp dom(b_{i}) = ∅ ∀i ∈ 1..n}{p ↦ [l_{i} = ς(x_{i})b_{i}^{i∈1..n}] : P roc}

The COQ formalization of the well-formed relation is its natural translation as an inductive definition well_formed, given table 16. well_formed is defined for Term and not dbterms. We must insure than for every term a, (T erm a) holds in the COQ definition.

5.2 Inversion

In the activity of proofs, inversion theorems are as important as induction schemes. In the usual cases, inversion theorems automatically generated by the proof assistants are those expected because the syntax of the calculi are defined in terms of a least fixed point. In our formalism, binders are functions on top

Table 17. Formalization of well_formed in COQ

flag =^{def} Exp | P roc

well_formed : dbterms → flag → P rop :=

⋯

Well_Res: ∀a : T erm.∀p : ref.∀T : flag.(well_formed a T) ⇒
p ∈ dom(a) ⇒ (well_formed νp.a T).
⋯

of a de Bruijn syntax thus from the equality νp.a = νq.b it is not possible to deduce than p = q and a = b. If the inversion theorems generated by COQ are used roughly they introduced news terms not directly related to anything in the proof. In table 18 we present the inversion theorem for the Well_Res constructor of the well_formed property generated by COQ ^{3}.

Table 18. Inversion lemma for well_formed generated by COQ

∀P : dbterm → flag → P rop. ∀a : T erm.∀p : ref.∀T : flag. ⟨∀q : names.∀b : T erm. νp.a = νq.b ⇒ q ∈ dom(b) ⇒ (well_formed b T) ⇒ (P a T)⟩

⇒ (well_formed νp.a T) ⇒ (P a T).

In a proof in which (well_formed νp.a T) is amongst the assumptions, using this theorem will not add (well_formed a T) in the hypothesis as expected. Similarly to induction schemes, the right inversion lemmas must be proved. Fortunately, it is sufficient to derive a specialized lemma for each constructors of the inductive definition. Then the COQ system provides tactics to use them properly^{4}. Because we can produce one lemma for each constructor, their formulation remains simple (see table 19 as an example).

Table 19. Inversion lemma for the Well_Res constructor

Lemma well_res_inv: ∀P : dbterm → flag → P rop.
∀a : T erm.∀p : ref.∀T : flag

(p ∈ dom(a) ⇒ (well_formed a T) ⇒ (P a T)) ⇒ (well_formed νp.a T) ⇒ (P a T).

To prove mres_inv we use a property stating than if νp.a = νp.b holds then a = b holds (such properties has to be proved for each of our binders). To complete the proof, we must show that if (well_formed a T) holds for a term a

3 The COQ system generates a general inversion theorem for well_formed; this is a

specialized version 4 inversion hyp using lemma

then (well_formed a[p/q] T) holds for any q and any p such that p ∉ Q for a finite set Q. In other words, we need to prove than well_formed is closed under reference (name in general) renaming. Again, this is not surprising. This property of the relation well_formed should also be checked when we are reasoning up to α-conversion during informal proofs, through this is most often omitted.

6 Subject reduction theorem

We show that well_formed terms are closed for the →_{red} relation. The formulation of this theorem (see table 20) is exactly the same as its unmechanized version appearing in [GH98]. The proof is done by induction on →_{red} using the extended induction theorem (see table 15). For each induction case, there is an hypothesis of the form (well_formed a T). We use our inversion lemmas to extract informations on sub-terms of a from it.

Table 20. Subject reduction theorem

Theorem srt:

∀a, b : dbterm.∀T : flag. (well_formed a T) ⇒ (a →_{red} b) ⇒
(well_formed b T) ∧ dom(a) = dom(b).

The proof of the theorem is very closed to the informal proof with implicit renamings of bound names. We do not manipulate de Bruijn indices neither are we doing α-renaming. All the lemmas used during the proof have a semantic contents.

7 Discussion and related work

The size of the different parts of the COQ code is summarize in the table below. In the column of Term we consider all the formalizations and proofs necessary for using the Terms. It includes the properties for the α-conversion and the renaming, the proofs of the extended induction principles the Term property most of the lemmas we have proved with the theorem Term_induction. We classify in the column of well_formed and →_{red} all the COQ codes which deal with the corresponding property (induction schemes, inversion lemmas, behavior of Subst_{∗} and dom). The srt column stand for the subject reduction theorem COQ codes part and the total column include all the previous ones plus some general lemmas (mainly set theory theorems) which do not use de Bruijn indices.

Term well_formed →_{red} srt total
lines of COQ code 7 700  2 400  2 500 1000 14 600
% of de Bruijn code 65%  10%  25%  -  40%

The percentage of the de Bruijn code in proofs is high during the setting of this technique. In fact, large de Bruijn codes mainly concern the Abst and Inst functions. But, once we have completely mastered the behaviors of Terms we do not use de Bruijn indices.

Given a property P : T erm → … → T erm → P rop, we must show that there exists a finite set X such that m ∉ X ⇒ (P a_{1} … a_{n}) ⇒ (P a_{1}[m/n] … a_{n}[m/n]) to get an induction principle which internalizes name renaming and the expected inversion lemmas. Checking that P is closed by renaming of names can be laborious in COQ whereas this is assumed for on paper proofs. Moreover, as we have experimented during this development, it clears the way for further proofs on the P property.

Related work. Among all the works formalizing the variable-binding operators in calculi none, as far as we know, uses the technique we have used here. Daniel Hirschkoff has encoded a polyadic π-calculus with de Bruijn numbers and proved many bisimulation results [Hir97]. Bruno Barras [Bar95] formalizes COQ in COQ with de Bruijn indices. In both approaches de Bruijn indices appear in almost all theorems and specifications. We think this is not natural. L. Henry-Gréard [Hen98] uses R. Pollack and J. McKinna technique [MP93] to formalize the π-calculus and prove a subject reduction theorem for it. In this technique, closer to the on paper formalism, there are two kinds of names, one for free ones and another for bound one. We think this is not completely natural. J. Despeyroux has investigated a higher-order approach in which the lambda abstraction of the logic is used for binding free variables of the calculus [Des]. See [DH94], for a general approach of this technique in COQ. F. Honsel, M. Miculan and I. Scagnetto [FI98] have encoded the π-calculus in COQ following a higher order approach. They use Co inductive types in their encoding of bisimulation. Although second order techniques are very efficient, we think that proofs using these techniques are very different from proofs on paper.

8 Conclusion and future work

We have formalized a concurrent object calculus in the COQ system with names in binders using a technique proposed by A. Gordon [Gor94]. We have shown that defining properties on Terms, namely those who formalize the concς-calculus in the COQ system, is very natural and easy because we just need to rewrite them using the COQ syntax. Under the assumption that a given property P is invariant under the renaming of names, the induction theorem generated by COQ for P can be strengthened to internalize α-renaming of bound variables. In spite of our syntax is not generated by a last fixed point we have inversion lemmas for P but they must be proved. The proofs of these theorems as the proof of the subject reduction theorem, are de Bruijn indices free. Moreover, the proofs dealing with real property of the calculus follow the general guideline of their on paper matching piece.

The main drawback of this approach is that each time we have to define functions on Terms we have to define them on dbterms first, then prove that they behave as expected on Terms. We believe that with a good understanding of the behavior of a function on Terms, it is not hard to give its definition on dbterms. We claim that this weakness does not overcome the advantages of the method. In fact, new functions on our syntax will probably use functions we have already defined, allowing re-use of our COQ proofs (as it is done for the function Subst_{∗} which appears in →_{red}).

For property P, the strengthened induction theorems could be a large term. It is interesting to develop tools for generating it automatically because this extended induction scheme is mechanically derivable (not provable) from P. Another reasonable development could be to include tactics for automating, on Terms, the computation steps of functions. We have done some preliminary work in this direction.

Acknowledgments I specially thank Joëlle Despeyroux for enlightening discussions about this work.

References

[AC96] Martin Abadi and Luca Cardelli. A Theory of Objects. Monographs in Computer Science. Springer-Verlag, 1996.

[Bar95] B. Barras. Coq en Coq. Mémoire du DEA informatique, mathématiques et applications, École Polytechnique, 1995. INRIA research report RR-3026, October 1996.

[BBC^{+}97] Janet Bertot, Yves Bertot, Yann Coscoy, Healfdene Goguen, and Francis Montagnac. User guide to the CtCoq proof environment, October 1997. Inria technical report, RT-0210.

[dB94] N.G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In J.H. Geuvers R.P. Nederpelt and R.C. de Vrijer, editors, Selected Papers on Automath, volume 133, pages 375–388. Studies in Logic, 1994. Reprinted.

[Des] Joëlle Despeyroux. A higher-order specification of the pi-calculus. Presented at the Modelisation and Verification seminar, Marseille, Dec 98. Submitted for publication, March.

[DH94] Joëlle Despeyroux and André Hirschowitz. Higher-order syntax and induction in Coq. In F. Pfenning, editor, Proceedings of the fifth Int. Conf. on Logic Programming and Automated Reasoning (LPAR 94), volume 822, pages 159–173. Springer-Verlag LNAI, July 1994. Also appears as INRIA Research Report RR-2292 (June 1994).

[FI98] M.Miculan F.Honsell and I.Scagnetto. Pi calculus in (co)inductive type theories. Technical report, Universita‘ di Udine, September 1998.

[GH98] A. Gordon and P. Hankin. A concurrent object calculus: reduction and typing. In Proceedings of the HLCL’98 Conference. Elsevier ENTCS, 1998.

[Gil00] Guillaume Gillard. A full formalization of a concurrent object calculus up to alpha-conversion. draft, January 2000. Available at

//ftp-sop.inria.fr/certilab/ps/conc_calculus.ps.

[Gor94] A. Gordon. A mechanisation of name-carrying syntax up to alphaconversion. In Proceedings of the 6th int. workshop on Higher Order Logic Theorem Proving and its Applications, Vancouver, Springer-Verlag LNCS 780, pages 413–425, 1994.

[Hen98] Loïc Henry_Greard. A proof of type preservation for the pi-calculus in Coq. Research Report RR-3698, Inria, December 1998. Also available in the Coq Contrib library.

[Hir97] Daniel Hirschkoff. A full formalization of pi-calculus theory in the Calculus of Constructions. In Amy Felty and Elsa Gunter, editors, Proceedings of the International Conference on Theorem Proving in Higher Order Logics, Murray Hill, New Jersey, August 1997.

[MP93] James McKinna and Robert Pollack. Pure Type Sytems formalized. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 289–305. Springer-Verlag LNCS 664, March 1993.

[MPW92] R. Milner, R. Parrow, and J. Walker. A calculus of mobile processes, (part I and II). Information and Computation, 100:1–77, 1992.

[Wer94] B. Werner. Une Théorie des Constructions Inductives. PhD thesis, Université Paris VII, Mai. 1994.