Inheritance of proofs

Inheritance of Proofs

Martin HofmannArbeitsgruppe Logik und mathematische Grundlagen der Informatik, Fachbereich Mathematik, Technische Hoch-schule Darmstadt, Schloßgartenstr. 7, D-64289 Darmstadt, Germany

Wolfgang NaraschewskiInstitut fur Informatik, Technische Universitat Munchen, Arcisstr. 21, D-80290 Munchen, Germany

Martin SteffenInstitut fur Informatik, Christian-Albrechts-Universitat zu Kiel, Preußerstr. 1-9, D-24105 Kiel, Germany

Terry StroupLehrstuhl fur Informatik VII, Friedrich-Alexander-Universitat Erlangen-Nurnberg, Martensstr. 3, D-91058 Erlangen,Germany

The Curry-Howard isomorphism, a fundamental prop-erty shared by many type theories, establishes a di-rect correspondence between programs and proofs.This suggests that the same structuring principles thatease programming should be useful for proving as well.To exploit object-oriented structuring mechanisms forverification, we extend the object-model of Pierce andTurner, based on the higher-order typed λ-calculus F ω≤,with a logical component.

By enriching the (functional) signature of objectswith a specification, methods and their correctnessproofs are packed together in objects. The uniformtreatment of methods and proofs gives rise in a naturalway to object-oriented proving principles — includinginheritance of proofs, late binding of proofs, and encap-sulation of proofs — as analogues to object-orientedprogramming principles. We have used Lego, a type-theoretic proof checker, to explore the feasibility of thisapproach. c© 1998 John Wiley & Sons, Inc.

1. Introduction

Many programming languages have been developedto ease modular and structured design of programs. Thepopularity of powerful structuring techniques, includ-ing object-oriented ones, is a convincing argument thatthose mechanisms support the programming task. De-pending on the programming style, they cater to divide-and-conquer strategies for breaking down large programsinto abstract data types, modules, objects, etc. Since theresulting components ideally mirror the decompositionof the problem into conceptually self-contained units, itis natural to organize verification along the structure ofthe programs.

Received January 28, 1997; revised July 25, 1997; accepted October3, 1997

c© 1998 John Wiley & Sons, Inc.

In this paper we apply this idea to object-orientationby showing that specification and verification can be or-ganized along the class hierarchy of object-oriented pro-grams and in particular that inheritance applies to proofsas well.

Our approach is based on a functional model ofobject-orientation. This means that we treat messagepassing as function application and classes as recordsof functions implementing the methods. In this way weavoid the problems involved with reasoning about localstate, for example aliasing, and can focus on the centralissues raised by inheritance and late binding. We believethat the ideas presented in this paper can be generalisedto a stateful model of object-orientation but acknowl-edge that more research would be necessary to achievethis goal.

To accomplish object-oriented verification we embedPierce and Turner’s object model [48] into the ExtendedCalculus of Constructions (ECC) [34] — a type theory inwhich programs and proofs, as well as types and specifi-cations coexist and can be interleaved. A particular fea-ture of type theories like ECC is that logical propositionsare treated as (particular) types having their proofs as el-ements; the so-called Curry-Howard isomorphism.

This means that in principle structuring mechanismsthat apply to programs and types scale up to proofs andspecifications. Although the Curry-Howard isomorphismserves as a guideline for generalizing the programmingmechanisms to proofs, several nontrivial novel problemsarise in the context of verification, e.g., the treatment of“self proofs” in Section 3.

Beyond the uniform treatment of programs andproofs, a further advantage of type theory is that imple-mentations are available which equip type theory with a

THEORY AND PRACTICE OF OBJECT SYSTEMS, Vol. 4(1), 51–69 1998 CCC 1074–3227/98/010051-19

front-end for the interactive goal-directed developmentof proofs and programs. We have used the Lego imple-mentation of ECC to carry out the proofs of all the neces-sary meta-properties and for the verification of a simpleclass hierarchy.

Our work is closely related to the construction de-veloped by Hofmann and Pierce [24] and can be seenas a further development and elaboration of ideas ex-pressed there. In particular, our approach builds upon theequational axiomatization of coercion and update and onthe idea of “inheriting proofs” introduced there. Apartfrom providing a formal type-theoretic underpinning forobject-oriented verification, including a Lego formaliza-tion, the present paper extends [24] by providing a moregeneral framework for the specification and verificationof late-binding methods, which avoids including imple-mentation details in specifications as was done in [24];see Section 3 for details. Moreover, we explain how β-reduction on proof terms can be used to eliminate theconsistency assumptions on specifications which wereneeded in [24]. Finally, the treatment of generic proofmethods is new.

The remainder of the paper is organized as follows:after a brief review of Lego, we present in Section 2an encoding of object-oriented programs in Lego basedon F ω≤’s functional model of object-oriented languages,and enriched by verification. The straightforward exten-sion, though, fails to capture all subtleties involved in theverification of late binding methods. Hence in Section 3we modify the encoding to overcome the limitations ofthe first attempt. In the concluding Section 4 we discussrelated and further work.

We assume some acquaintance with typed λ-calculiand functional models of object-oriented languages. Agood reference on both topics is Mitchell’s book [39]; seealso Cardelli’s handbook article [9] for general referenceon type systems for programming languages. Knowledgeof Lego or a similar type-theoretic proof-checker will behelpful, but is not strictly necessary. A detailed introduc-tion to Lego can be found in the manual [36] or in theweb resources [33]. F ω≤’s object-model which forms thebasis of our approach is presented in Pierce and Turner[48] and Hofmann and Pierce [25].

2. Verification of Object-Oriented Programsin Lego

2.1. The Lego Proof Assistant

The Lego proof assistant [36] is an interactive, type-theoretic proof checker. It implements the Extended Cal-culus of Constructions (ECC) and a family of weaker, re-lated type theories. The system includes a strongly typedfunctional programming language as well as a higher-

order intuitionistic logic. The ECC uses a predicativehierarchy of universes for programming and an impred-icative universe for logical propositions.1

Lego offers inductive definitions of data types to-gether with induction principles. By means of its refine-ment mechanism, based on first-order unification, it sup-ports interactive, goal-directed proof development in anatural-deduction style. Working with Lego is supportedby local and global definitions and by implicit arguments,which allow the user to omit automatically synthesiz-able function arguments. Lego also offers arbitrary user-defined reduction rules, the soundness of which has to beverified externally, of course. We will make use of thisfeature in the definition of existential types with depen-dent elimination rule.

For the purpose of understanding this paper it shouldbe enough to know that Lego supports an extension of Fω

by higher-order logic with explicit proof objects. That isto say, if A is a type of Fω, we can form in Lego the typeA → ? of types depending on A, in particular of predi-cates over A; if P : A → ? and a : A then P(a) is a type;the type of proofs of P(a). Elements of such proof typescan be constructed interactively in a goal-directed fash-ion. Types and predicates can be packed together usingΣ-types; for example Σx : A.P(x) has as elements pairs〈x, p〉 where x : A and p : P(x). If z : Σx : A.P(x) thenz.1 : A and z.2 : P(z.1). To ease readability, we use de-pendent records as syntactic sugar for (nested) Σ-types.In the above example we could write [c1 : A, c2 : P(c1)]for the dependent record type. The corresponding inhab-itants are of the form [c1 = a, c2 = p] where a : A andp : P(a), i.e., p is a proof of P(a). At the moment, Lego’stype theory does not provide subtyping; we simulate asubtyping judgement A ≤ B by a type whose membersare triples consisting of a coercion from A to B, an up-date function and a proof that these two functions satisfycertain equations. See Section 2.3.1. for details.

Conventions. All definitions and proofs of this paperhave been machine-checked by Lego.2 To ease humanreading, though, we do not employ Lego-syntax; insteadwe write terms in a more conventional notation, usingλ for abstraction and ∀ for Lego’s dependent Π-type.For the impredicative universe Prop of logical propo-sitions we write ? and dependent records are notedas indicated above. We fall back upon definitions pro-vided by the Lego-library [27] whenever appropriate. Ifnot immediately obvious, these definitions will be in-formally explained in the text so that no knowledge ofthe Lego library is required. We further use the key-word let for local definitions, write ( , ) for the non-dependent pairing function with surjective pairing fromthe library lib prop/lib prod.l. We denote Leibnizequality from lib eq.l by =L , allowing ourselves in-fix notation.3 The inductive natural numbers of the Lego-library lib prop/lib nat/lib nat.l are written as

52 THEORY AND PRACTICE OF OBJECT SYSTEMS–1998

nat and we assume tacitly the usual operators to be avail-able and standard properties to hold.

Lego supports implicit syntax to simplify definitions,synthesizing omitted arguments on its own. As in Lego,we replace a declaration x : A in a ∀-type or in a λ-abstraction by x | A indicating that x is an implicit ar-gument. In most definitions, we do not give the wholeexpression as a λ-term, but put some leading abstrac-tions into the text. Free variables in types are meant tobe universally quantified. Finally, we elide conjunctionsbetween displayed equations. Apart from these conven-tions, though, all definitions are complete and can bedirectly translated into Lego.

2.2. The F ω≤ Object Model

In recent years, a number of typed λ-calculi have beeninvestigated as foundation of typed object-oriented lan-guages. The line of research started with Cardelli andWegner’s proposal [10] for the typed object-orientedtoy language Fun based on F≤, an extension of thesecond-order polymorphic λ-calculus [19, 50] by sub-types. Cardelli and Wegner proposed to model objects asrecords of their methods. The language Fun has spawneda number of different calculi of varying complexity. Anoverview can be found in [18] or in Fisher’s thesis [17],a collection of relevant papers in [21].

For our purpose of integrating an object calculus intoa logical framework, one particular formal system, thesystem F ω≤ [52] is a suitable basis, since it avoids thecomplexity of calculi with recursive types [6, 38].

F ω≤, the extension of F≤ by type operators of arbi-trary order, has been proposed by Pierce and Turner[47, 48, 25] as a core calculus for object-oriented lan-guages in the style of Smalltalk [20]. In the following,we informally recapitulate the representation of object-oriented programming concepts in this framework. Amore detailed account of representing object-orientedprograms in F ω≤ can be found in [46, 48].

According to [48] an object is a collection of opera-tions, working on an internal state. Both state and oper-ations are encapsulated or hidden inside the object, andaccess is controlled by the interface. In the object modelwe use, encapsulation is represented by existential quan-tification; encapsulation by existential quantification wasfirst proposed by [40].

We call the type of the internal state the representationtype of the object. The type of the operations, abstractedover the representation type, is called the object’s sig-nature Sig : ? → ?. See the definition of SigPoint inSection 2.3.2. for an example of such a signature. Usu-ally, for Rep : ? the type Sig Rep is a record of functionswith argument of type Rep. The type of objects withsignature Sig : ? → ? is defined as

Object(Sig) = ∃ Rep : ? . [state : Rep, ops : Sig Rep]

Using the introduction rule for existential types we canconstruct an element of type Object(Sig) from some rep-resentation type Rep, a state state : Rep and an imple-mentation ops : Sig Rep of the operations. Existentialelimination, on the other hand, allows one (under a co-variance condition on the form of Sig explained in detailin [25]) to define a generic method of type Sig Objectwhich when applied to an object applies its internalmethods to its state and returns the packaged result.

In class-based languages, a class serves as a blueprintfor objects and can be used in two ways: First, to createnew objects sharing the representation and implemen-tation common to the class: the classes instances. Sec-ond, to define new subclasses incrementally by inheri-tance, where (parts of) the definitions of the old super-class may be used. By inheritance, some methods maybe re-implemented and overridden or, by enriching thesignature, new methods may be added to unchanged, in-herited ones.

An important intricacy are the so-called self-methods.This concept, popular since Simula and Smalltalk, per-mits methods to be defined in terms of other methods ofthe same class. What makes it difficult to model is thatself does not refer statically to the methods implementedby the class. If a method refers via self to another methodand gets inherited by a subclass, then self no longer refersto the operations of the superclass, from which it was in-herited, but dynamically to the ones of the new class; incase one of the methods is re-implemented, all others re-ferring to it via self are modified as well. This is knownas dynamic binding of methods or late binding.

The last ingredient we mention is subtyping. Subtyp-ing constitutes an order relation on types, where S ≤ Tmeans that an element of type S can be regarded as anelement of T and thus safely be used when an inhabitantof T is expected. This is known as substitutability or sub-sumption. Subtyping must not be confused with inheri-tance: Inheritance is the construction of a new subclass,whereas subtyping is concerned with the use of objects— or terms in general. Although inheritance and sub-typing are different, there is a connection between themin this model: the type of any instance of a subclass isa subtype of the type of any instance of the superclass.Subclasses and superclasses themselves, however, are notrelated by subtyping (see, e.g., [12]).

2.3. Encoding of Object-Oriented Programs

The system F ω≤ is sufficiently expressive to modelobject-oriented programs but, lacking dependent types,neither to specify their behavior nor to reason about theminternally. We transfer the F ω≤ object-model to Lego andextend it in such a way that the types of the objects willnot only include the functional types of the operations,but also a specification of their behavior. The objects

THEORY AND PRACTICE OF OBJECT SYSTEMS–1998 53

then contain correctness proofs in addition to the imple-mentation of the operations.

Apart from subtyping, transferring F ω≤’s object-oriented programming model to Lego is trivial, since inthe λ-cube [5] the ω-order λ-calculus F ω [19] is a subcal-culus of the Extended Calculus of Constructions (moreprecisely of the pure Calculus of Constructions). Sub-typing, though an integral part of F ω≤, is neither presentin the Extended Calculus of Constructions nor in Lego,so we have to find an adequate representation.

2.3.1. Subtyping. A type S being a subtype of T, writ-ten S ≤ T, means that it is safe to use terms of thesmaller type in all cases where a term of the bigger typeis expected. This is expressed by subsumption. Conven-tionally, the subtype relation can be captured by so-calledcoercion functions, where the statement S ≤ T is repre-sented as a function f : S → T. If we view the type Sas a more refined version of T, the coercion functionextracts the T-part of elements of S. As shown in [24],this simple representation is not enough to model updatetogether with subtype polymorphism in a functional set-ting. To account for updating, S ≤ T is represented asa pair of functions, say get and put, with get : S → Tand put : S → T → S. The function get plays the roleof the coercion function, extracting the T-part of ele-ments of S, and put takes as first argument a value oftype S and overwrites its T-part with the second argu-ment, without altering the rest. For a restricted set oftypes the functions get and put can be generated auto-matically. A model where subtyping is interpreted in thisway and where the examples of this paper can be rep-resented has been developed for a restriction of F≤ in[24]. The interpretation of get and put as extraction andupdate functions is captured by the three equations ofthe following definition.

Definition Laws for get and put [24]. Assume im-plicitly two types S and T and assume further two func-tions get : S → T and put : S → T → S. The laws for getand put are defined as the following equations:

get (put s t) =L t (1)

put s (get s) =L s (2)

put (put s t1) t2 =L put s t2 (3)

The Lego-representation GetPutLaws of these equa-tions abstracted over S, T, get, and put has type∀S | ? . ∀T | ? . (S → T) → (S → T → S) → ?. We useit to define the subtype relation, where Lego’s |-syntaxfor implicit arguments allows us to omit mentioning thefirst two arguments of GetPutLaws:

Definition Subtype relation. Assume the typesS : ? and T : ?. The subtype relation is then defined as:

S ≤ Tdef= [ get : S → T,

put : S → T → S,gpOK : GetPutLaws get put ]

The elements gp of a type S ≤ T are triples, consistingof two functions get and put, and a proof gpOK that theysatisfy the required laws. Reflexivity and transitivity ofthe subtype relation are easily established.

Lemma 1. The subtyping relation is a pre-order in thesense that there are terms refl≤ : ∀S : ? . S ≤ S andtrans≤ : ∀S, T, U | ? . (S ≤ T) → (T ≤ U) → (S ≤ U).

Proof. For reflexivity, define the two functions as theidentity and the second projection. The GetPutLaws areimmediate by reflexivity of Leibniz’s equality.

For transitivity, let gpS≤T be a proof for S ≤ T andgpT≤U for T ≤ U. Define the extraction function fromS to U as the composition of gpS≤T.get with gpT≤U.get.The update function is composed as

λs : S. λu : U.gpS≤T.put s (gpT≤U.put (gpS≤T.get s) u).

Proving the respective laws is straightforward.

We do not address coherence of this notion of subtyp-ing here, so — strictly speaking — we model F ω≤ deriva-tions not judgements. In principle, Curien and Ghelli’scoherence proof for F≤ with explicit coercions [14]should be applicable to the present situation.

2.3.2. Objects. Intuitively, the inclusion of specifica-tions in the interface of objects is straightforward. Inaddition to the functional signature Sig : ? → ?, the in-terface needs a component Spec which specifies prop-erties of the object in terms of its operations and thushas type ∀ Rep : ? . (Sig Rep) → ? . Recall that ? isthe kind of datatypes and propositions. Given a rep-resentation type Rep, the body of an object has type[state : Rep, ops : Sig Rep, prfs : Spec Rep ops] and consistsof a state, the operations, and a proof that they satisfythe specification.

But how to achieve encapsulation? In the informal ex-planation in Section 2.2, we used F ω≤’s existential quan-tifier to hide the internal state and the operations. Usingthe standard impredicative encoding

∃ = λP : ? → ? . ∀C : ? . (∀R : ? . (P R) → C) → C

of the weak sum, then, as explained in [48] and [25], wecan define a generic method meths of type Sig Object.However, although every object embodies a proof thatits methods satisfy the specification Spec, we cannot ob-tain an externalized version of the proofs, i.e., prove


Spec Object meths. The reason is that the (definable)elimination function associated with the impredicativeencoding is too weak as can be seen from its type

∀C : ? . (∀R : ? . (P R) → C) → (∃R : ? . P R) → C,

where P : ? → ? is an arbitrary type operator. (Weuse the more familiar notation ∃R : ? . P R instead of∃(λR : ? . P R).) Roughly speaking, this elimination ruleallows us to define a function of type (∃R : ? . P R) → Cprovided we specify it on canonical elements. It doesnot allow us to prove anything about elements of type∃R : ? . P R, i.e., to define a dependent function of type∀o : (∃R : ? . P R) . C o where C : (∃R : ? . P R) → ?.

The solution we propose is to axiomatically assumean existential quantifier together with the usual introduc-tion rule and a dependent elimination rule which over-comes the shortcoming of the impredicative encoding.Of course, the soundness of such an extension has to bevalidated externally as we will do below.

Definition Existential quantification. The forma-tion, the introduction, and the elimination rule for thetype constructor ∃ are declared as follows:

∃ : (? → ?) → ?

pack : ∀P : ? → ? . ∀R : ? . (P R) → ∃R : ? . P R

open : ∀P : ? → ? . ∀C : (∃R : ? . P R) → ? .(∀R : ? . ∀x : P R. (C (pack P R x))) →

∀o : (∃R : ? . P R). C o

Assume predicates P : ? → ? and C : (∃R : ? . P R) →? and a function f : ∀R : ? . ∀x : P R. C (pack P R x).Assume further R : ? and x : P R. The reduction rule isthen defined as:

open P C f (pack P R x) ⇒ f R x

This existential quantifier can be soundly interpretedin the PER/ω-set model of the ECC [34] as follows. If Fis a function mapping partial equivalence relations on N(PERs) to PERs. Define ∃(F) as the symmetric, transitiveclosure of the union of the F(R) as R ranges over the setof PERs. This is the least upper bound of the F(R) inthe complete lattice of the PERs ordered by set-theoreticinclusion. The pack-construct can then be modelled as aninclusion map, i.e., we have F(R) ⊆ ∃(F) for each R. Tointerpret open we assume a family of PERs indexed overthe quotient of ∃(F) or equivalently a PER C(n) for eachn in the domain of ∃(F) and satisfying C(n) = C(n′)whenever n and n′ are related by ∃(F). The premise toopen corresponds in the PER model to an algorithm esuch that for each PER R, whenever n and n′ are relatedin F(R) then e(n) and e(n′) are defined and related inC(n)(= C(n′)). Now, if n and n′ are related in ∃(R) itfollows by induction on the length of a path relating nand n′ that e(n) and e(n′) are both defined and related inC(n). So e itself yields the interpretation of open.

Now we can define the type of objects, using the de-clared existential quantifier.

Definition Type of objects. Assuming a signatureSig of type ? → ? and a specification Spec of type∀ Rep : ? . (Sig Rep) → ?, the type of objects is givenas:

Objectdef= ∃ Rep : ? .

[state : Rep, ops : Sig Rep, prfs : Spec Rep ops]

With the existential quantifier as top-level constructor,objects are built by the existential introduction rule. Toease the presentation, we define a term for construct-ing objects with the help of the existential introductionoperator pack.

Definition Object introduction. Assuming implic-itly a representation type Rep, a signature Sig, and aspecification Spec, the function ObjectIntro for object in-troduction is defined as:

ObjectIntrodef=

λ mystate : Rep .λ myops : Sig Rep .

λ myprfs : Spec Rep myops .pack (λ Rep : ? . [ state : Rep,

ops : Sig Rep,prfs : Spec Rep ops ])

Rep[ state = mystate,

ops = myops,prfs = myprfs ]

: Rep → ∀ myops : Sig Rep . (Spec Rep myops) →Object Sig Spec

Let’s illustrate these definitions of objects with the stan-dard example of points. For the sake of discussion, ourpoints have one coordinate in nat admitting examina-tion by getX , overwriting by setX , and augmentation byinc1. A natural choice, though not the only possible one,for the internal representation type is the type of naturalnumbers itself.

Example 1 Points. The signature SigPoint of points isthe product of the types of the operations getX, setX, andinc1, abstracted over the representation type Rep:

SigPointdef= λ Rep : ? . [ getX : Rep → nat,

setX : Rep → nat → Rep,inc1 : Rep → Rep ]

For the specification of points, assume a representationtype Rep and operations ops conforming to the signatureof type SigPoint Rep. To simplify the presentation, thespecification SpecPoint consists of only two equations:

SpecPointdef=

ops.getX(ops.setX r n) =L nops.getX(ops.inc1 r) =L (ops.getX r) + 1


The type of points Point is defined using the type con-structor Object.

Pointdef= Object SigPoint SpecPoint

Let us define a concrete object MyPoint : Point with rep-resentation type nat and initial value 3 by the object in-troduction rule ObjectIntro. The operations are imple-mented as:

opsPointdef= [ getX = λn : nat . n,

setX = λn : nat . λm : nat . m,inc1 = λn : nat . n + 1 ]

: SigPoint nat .

The pair prfsPoint : SpecPoint nat opsPoint of correctnessproofs for the two equations is immediate by reflexivityof Leibniz’s equality. Putting it all together by object in-troduction yields a concrete point of type Point:

MyPointdef= ObjectIntro 3 opsPoint prfsPoint

2.3.3. Generic methods. So far, we have means to en-capsulate the state of objects by existential quantifica-tion. As mentioned before, we also need a mechanismto gain disciplined access to the objects, using the op-erations and the proofs mentioned in the interface. Thegeneric methods are functions that open the objects anduse the internal operations to perform the requestedmanipulations. If the operations ops of an object havetype Sig Rep for some Rep : ?, the type of the genericfunctional methods meths is Sig (Object Sig Spec). Thegeneric version of proofs of Spec Rep ops then hastype Spec (Object Sig Spec) meths. In the point exam-ple, the generic methods methsPoint have the typeSigPoint Point = [ getX : Point → nat, setX : Point →nat → Point, inc1 : Point → Point ] and the generic ver-sion of the first equation of the specification is for in-stance methsPoint.getX(methsPoint.setX p n) =L n. Ascan be seen from their types, the generic methods are tobe defined generically for all objects, i.e., independentlyof any internal implementation.

The generic methods discussed above invoke the inter-nal operations and proofs of objects with a specific inter-face. Subtyping should facilitate the use of generic meth-ods for more refined objects, e.g., the application of thepoints’ methods to colored points, providing additionaloperations and proofs dealing with the color. It is notenough, however, to be able to apply the generic methodsto more refined objects, as the state-modifying methodshave to return objects of the subtype, too. For exam-ple, the type of the method overwriting the x-coordinateof points should be ∀P ≤ Point . P → nat → P. It iswell known [46] that only trivial functions inhabit thistype. The solution proposed for F ω≤ is to use the subtypepolymorphism not on the type of objects, but on theirsignature, resulting in ∀ Sig ≤ SigPoint . (Object Sig) →

nat → (Object Sig) as the type for the setX method. InSection 2.3.1. we have encoded the subtype relation aspairs of extraction and update functions. Since for theabove subtype relation on the signatures, the update partis not needed, we represent the relation simply by anextraction function.

Example 2 Generic methods for points. Assume im-plicitly a signature Sig : ? → ? and a specificationSpec : ∀ Rep : ? . (Sig Rep) → ? together with a coercionco sig of type ∀ Rep | ? . (Sig Rep) → (SigPoint Rep). Thegeneric method Point′setX is defined as follows:

Point′setXdef=

λ o : Object Sig Spec .λ n : nat .open (λ Rep : ? . [ state : Rep,


(λ : Object Sig Spec . Object Sig Spec)(λ Rep : ? .λ stateopsprfs : [ state : Rep,

ops : Sig Rep,prfs : Spec Rep ops ].

ObjectIntro[state = (co sig stateopsprfs.ops). setX

stateopsprfs.state n,ops = stateopsprfs.ops,prfs = stateopsprfs.prfs ] )

o: (Object Sig Spec) → nat → (Object Sig Spec)

The methods Point′getX : (Object Sig Spec) → nat andPoint′inc1 : (Object Sig Spec) → (Object Sig Spec) can bedefined analogously.

In a similar way, the generic proof methods for pointsare obtained by opening the point and accessing the cor-responding internal proof. In contrast to the model ofPierce and Turner we have to deal with the proof-part aswell, which implies that in addition to the signature co-ercion co sig : ∀ Rep | ? . (Sig Rep) → (SigPoint Rep) werequire a specification coercion

co spec : ∀ Rep | ? . ∀ ops | Sig Rep .(Spec Rep ops) →

(SpecPoint Rep (co sig ops)) .

With these extraction functions we can define genericproof methods for the specification of points.

Example 3 Generic proof methods for points. Assumeimplicitly a signature Sig, a specification Spec, and co-ercion functions co sig and co spec. The generic proofmethod for the first equation is defined as follows:


Point′prf1def=

λ o : Object Sig Spec .λ n : nat .open (λ Rep : ? . [ state : Rep,


(λo : Object Sig Spec . Point′getX co sig(Point′setX co sig o n) =L n)

(λ Rep : ? .λ stateopsprfs : [ state : Rep,


let mystate = stateopsprfs.statemyprfs = co spec (stateopsprfs.prfs)

in myprfs.1 mystate n)o

: ∀o : Object Sig Spec . ∀n : nat .Point′getX co sig (Point′setX co sig o n) =L n

In the same way, the generic proof method Point′prf2of the second equation has type ∀o : Object Sig Spec .∀n : nat . Point′getX co sig (Point′inc1 co sig r) =L

(Point′getX co sig r) + 1 and can be defined analogously.We have illustrated the generic methods on the spe-

cific example of points. For a restricted set of signaturesit is possible to define the generic methods uniformly[25], namely for signatures of the form λ Rep : ? . Rep →(T Rep), where T is covariant in its argument Rep.

The restriction to covariant signatures excludes thedefinition of binary generic methods such as Point →Point → bool since they would need to compare the stateof two points of arbitrary representation types; but theseare hidden by the existential quantifier. This phenomenonhas been discussed already in the context of abstract datatypes in [40] and [37]. (Cf. [7] for a detailed discussionof problems related with binary methods in typed object-oriented programming languages.)

In this example we were able to define the genericfunctional methods, as the signature is basically ofthe above form. Instead of SigPoint, we could haveused λ Rep : ? . Rep → [getX : nat, setX : nat → Rep,inc1 : Rep ] as well; for presentational purposes, we havechosen the form of signature given in the Example onPoints, above.

Similarly, a generic proof method with type Spec(Object Sig Spec) meths can only be defined if the spec-ification has the form of universally quantified clauseseach of which contains Rep in covariant position only.For example, if SpecPoint would contain the clause

∀r : Rep .∀r′ : Rep . (ops.getX r =L ops.getX r′) → (r =L r′)

then a generic proof method would state that two pointobjects with equal x-coordinate are equal. Note that thetype of r′ constitutes a contravariant occurrence of typeRep. Even if this property is locally satisfied by concreterepresentations it is unsound in its general form (think

of points with a color attribute which is blue in one rep-resentation and red in another one). We believe that therequired covariance condition on Spec can be formalisedin such a way that a uniform definition of generic proofmethods can be given along the lines of [25].

For the moment we circumvent this problem by givingan explicit definition of generic (proof) methods in eachcase.

2.3.4. Objects without logical components. In theprevious sections we have emphasized the benefit ofpacking programs and proofs together in the objects. Inthe context of formal verification the given argumentsare justified, but they don’t apply if the objects are to beexecuted. For this purpose the proofs are ballast; worsestill, they are big. As programs and proofs form a pair,we can jettison the proofs simply by projecting out theprograms. To take care of encapsulation, we open the ob-jects first, then extract the programs, and finally repackthe objects without the proofs. The type of the resultingtrim objects coincides with the one in [48].

Definition Type of objects without logical compo-nent. Assuming a signature Sig : ? → ? the type of ob-jects without proof component is given as:

Object effdef= ∃ Rep : ? . [state : Rep, ops : Sig Rep]

Defining the function forget prfs of type ∀ Sig : ? → ? .∀ Spec : (∀ Rep : ? . (Sig Rep) → ?). (Object Sig Spec) →(Object eff Sig) which forgets the proof-part of objects,is analogous to defining generic methods.

Definition Objects without logical component.Assuming implicitly a representation type Rep, a signa-ture Sig, and a specification Spec, the term for forgettingthe proof component is defined as:

forget prfsdef=

λ o : Object Sig Spec .open (λ Rep : ? . [ state : Rep,


(λ : Object Sig Spec . Object eff Sig)(λ Rep : ? .λ stateopsprfs : [ state : Rep,


pack (λ Rep : ? . [state : Rep, ops : Sig Rep])Rep[ state = stateopsprfs.state

ops = stateopsprfs.ops ])o

: (Object Sig Spec) → (Object eff Sig)

Alternatively, we can view “inheritance of proofs”merely as a methodology for structuring informal proofson paper.


2.3.5. Classes. As mentioned in Section 2.2, a classdetermines the implementation of its instances. Since wehave extended the interface of objects with a specifica-tion, a class has to provide not only the code of the op-erations, but a proof of its correctness as well.

We cannot yet implement the class for a fixed repre-sentation type, say ClassR, since the mechanism of inher-itance may extend and change the representation type. Sothe signature and the specification both have to refer to arepresentation type Rep, as yet indeterminate. Of coursewe cannot expect to program non-trivial operations andproofs for an arbitrary representation type Rep. Con-straining the possible representation types to subtypes ofthe fixed ClassR gives the necessary connection betweenthe two types in terms of the extraction and update func-tion: the laws of get and put in Laws for get and put [24]above guarantee that the operations will behave correctlyon the ClassR part of its subtype Rep without compro-mising the rest. The representation type Rep remains pro-visional as long as we create subclasses by inheritance.It will be fixed, i.e., identified with the representationtype of the corresponding class, only when an instanceof the class is generated. Hence we could write the typeof a class with fixed representation type ClassR, signa-ture Sig, and specification Spec as ∀ Rep : ? . (Rep ≤ClassR) → [ops : Sig Rep, prfs : Spec Rep ops].

So far, though, we have not said a word aboutself-methods and self-proofs. The possibility of self-reference to operations and proofs in classes is the keyto the flexibility of inheritance. In this functional set-ting, self-reference is simply achieved by assuming selfas a variable of type [ops : Sig Rep, prfs : Spec Rep ops],i.e., the implementation is abstracted over this variable,giving classes the following type.

Definition Type of classes. Assume a representa-tion type ClassR : ?, a signature Sig : ? → ?, and aspecification Spec : ∀ Rep : ? . (Sig Rep) → ?. The typeof classes is given as:

Classdef=

∀ Rep : ? . (Rep ≤ ClassR) →[ops : Sig Rep, prfs : Spec Rep ops] →

[ops : Sig Rep, prfs : Spec Rep ops](self )

A fixed point operator will be used to resolve the func-tional abstraction on self at instantiation time; this willbe discussed in the following section. Again we illustratethe definition by our running example.

Example 4 Class of points. The type PointClass ofclasses of points with representation type nat, signatureSigPoint, and specification SpecPoint (cf. the Example onPoints, above) is built using the type constructor Class:

PointClassdef= Class nat SigPoint SpecPoint

We define a concrete class MyPointClass of typePointClass as pair of the operations and of their correct-

ness proofs. The abstraction over self enables referenceto the self-methods and self-proofs.

MyPointClassdef=

λ Rep : ? . λ gp : Rep ≤ nat .λ self : [ops : SigPoint Rep, prfs : SpecPoint Rep ops].

[ops = opsPointClass, prfs = prfsPointClass]

The operations of the class are implemented as the fol-lowing triple:

opsPointClass =[ getX = λr : Rep . gp.get r,

setX = λr : Rep . λn : nat . gp.put r n,inc1 = λr : Rep . self.ops.setX r

(self.ops.getX r) + 1 ]

Although the example may suggest that the two functionsget and put for the subtype relation were tailored to en-code the two methods getX and setX the contrary is true.As shown in [24] the functions get and put are canonicalin the sense that they make the basic manipulations of astate available: reading and updating it.

Finally, we have to prove the correctness of the oper-ations just defined, i.e., give an element prfsPointClassof type SpecPoint Rep opsPointClass. The first equationof the specification

opsPointClass.getX (opsPointClass.setX r n) =L n

only contains operations not depending on self . Usingtheir implementation it reduces to:

gp.get (gp.put r n) =L n

The equation coincides with the first law for get and put,accessible by gp.gpOK.1.

The specification’s second equation postulates the cor-rect behavior of the increment operation, which is definedin terms of self :

opsPointClass.getX (opsPointClass.inc1 r) =L

(opsPointClass.getX r) + 1

which β-reduces to

gp.get (self.ops.setX r (self.ops.getX r) + 1) =L

(gp.get r) + 1

This equation, though, is not provable in the present sit-uation. The reason is that there is no way to relate theimplementation of the methods — in the above equationthe function get as implementation of the getX method— with the operations referred to by self . In the cur-rent encoding of classes, a richer specification wouldnot help, since the necessary connection cannot evenbe specified. This does not imply that proofs about selfmethods are impossible at this stage. It is possible toprove equations involving only self methods, but not, asin the above equation, those involving both self and othermethods. Section 3 will discuss this problem and proposesolutions.


2.3.6. Instantiation. The instantiation operator new isa function that generates a new object when applied toa class and an initial value. As explained in the previoussection, a class does not provide an implementation ofobjects for a fixed representation type ClassR, but for anyrepresentation type Rep ≤ ClassR. At instantiation, therepresentation type becomes fixed, i.e., identified withClassR. In addition, classes are abstracted over the vari-able self . This dependency has to be resolved, ensuringthat self now refers to the class being instantiated.

In [47], this dependency was resolved using a fixedpoint operator. Although it is in principle possible to ex-tend Lego by general recursion, see, e.g., [49, 3], we haveopted for the simpler alternative of using the boundedfixpoints from [24]. This means that we replace an in-stance fix f where f : A → A by the n-fold iterationfn(basis) of f on a start value basis : A. This expressionyields the unique fixpoint of f provided fn is a con-stant function. Again following [24] we think that it is areasonable restriction that dependencies of methods onself be resolved after a fixed, input-independent numberof recursive unfoldings. For a more thorough discussionof bounded fixpoints we refer to op. cit. In Lego the n-fold iteration of a function is encoded using the iterationoperator nat iter of type ∀A | Type . A → (A → A) →nat → A as defined in the Lego-library.

Definition Instantiation. Assuming implicitly arepresentation type ClassR, a signature Sig, and a spec-ification Spec, the instantiation operator new is definedas:

newdef=

λ class : Class ClassR Sig Spec .λ state : ClassR .λ basis : [ops : Sig ClassR, prfs : Spec ClassR ops]λn : nat .

let opsprfs =nat iter basis

(class ClassR (refl≤ ClassR))n

in (ObjectIntro state opsprfs.ops opsprfs.prfs): (Class ClassR Sig Spec) → ClassR →[ops : Sig ClassR, prfs : Spec ClassR ops] → nat →

Object Sig Spec

This instantiation operator neither guarantees that af-ter the given number of function iterations the self-methods and self-proofs are resolved, nor that they areresolvable at all. To ensure this, the definition can easilybe modified so that the programmer has to prove thatnat iter basis (class ClassR (refl≤ ClassR)) n is indeeda fixed point of class ClassR (refl≤ ClassR). In Section 3we give a more refined definition of instantiation whichrequires the programmer to provide a proof that the it-eration is indeed a fixed point of the class. Also noticethat instantiation takes a correct implementation, namelybasis as an argument. In other words, we have to pro-

vide an implementation plus a correctness proof in thefirst place.

In a strongly normalising system like Lego the rule ofstrengthening is admissible. This means that if a term —be it a program or a proof — does not literally contain avariable (or an assumption), then it can by type-checkedwithout this variable (or assumption). This allows us touse the following semi-algorithm to compute an appro-priate iteration index n and to discharge the consistencyassumption basis.

• Given class ClassR (refl≤ ClassR) successivelycompute the β-normal forms of classi basis wherebasis :[ops : Sig ClassR, prfs : Spec ClassR ops] is a freshvariable.

• Stop when an index n is found such that the β normalform of classn basis does not contain basis literally.

Now, selfresolveddef= classn basis is a fixed point of

class and moreover, by strengthening, constitutes a prov-ably correct implementation of the specification Specnot depending on consistency of the latter. This semi-algorithm will always terminate if the function class doesnot contain circular dependencies on self either in thecode or in the proofs. We believe that this situation canin many cases also be recognized by a static analysis ofthe structure of possible calls to self.

Example 5 Instance of points. A concrete objectMyPointInstance with x-coordinate 3 is instantiated fromthe class PointClass by means of the instantiation op-erator new. Only two iterations are needed to resolvethe self-methods; thereafter the variable self has disap-peared. We can therefore apply the instantiation operatorto a variable basis and nevertheless obtain (by strength-ening) a closed and correct implementation:

basis : [ops : SigPoint nat, prfs : SpecPoint nat ops]

MyPointInstancedef= new MyPointClass 3 basis 2

We want to stress that this line of reasoning hinges on thefact that we have explicit proof objects and β-reductionon these. Without β-reduction the variable basis couldnever literally disappear.

2.3.7. Inheritance. Inheritance allows to define newclasses by means of already defined ones. As in the ob-ject model of F ω≤, inheritance is represented by a functioninherit which generates the subclass when applied to asuperclass and to a function build. The argument buildserves as an instruction how to construct the subclassfrom the implementation of the superclass.

Like any class, the subclass has to be implementedfor an arbitrary subtype Rep of its representation typeSubR. To use the implementation of the superclass inthe subclass, we have to ensure that the operations ofthe superclass work on Rep as well. A proof of SubR ≤


SuperR together with transitivity of the subtype relationsuffices.

Late binding requires that the variable self in theinherited operations and proofs be bound to the self -parameter of the present class. This is achieved by trans-forming the self -parameter using appropriate coercionfunctions between the signatures and the specifications.

Definition Inheritance. Assume implicitly a repre-sentation type SuperR : ?, a signature SuperSig : ? → ?,and a specification SuperSpec of the superclass, whichitself has type ∀ Rep : ? . (SuperSig Rep) → ?. In ad-dition, assume for the subclass a representation typeSubR, a signature SubSig, and a specification SubSpeccorrespondingly. Finally, assume a proof gpSubR≤SuperR

of type SubR ≤ SuperR and two coercion functionsco sig : ∀ Rep | ? . (SubSig Rep) → (SuperSig Rep)and co spec of type ∀ Rep | ? . ∀ ops | SubSig Rep .

(SubSpec Rep ops) → (SuperSpec Rep (co sig ops)). Theinheritance operator is then defined in Figure 1.

inheritdef=

λ SuperClass : Class SuperR SuperSig SuperSpec .λ build : ∀ Rep : ? . (Rep ≤ SubR) →

[ops : SuperSig Rep,prfs : SuperSpec Rep ops] → (super)

[ops : SubSig Rep,prfs : SubSpec Rep ops] → (self )

[ops : SubSig Rep, prfs : SubSpec Rep ops].( λ Rep : ? . λ gpRep≤SubR : Rep ≤ SubR .

λ self : [ops : SubSig Rep, prfs : SubSpec Rep ops].build Rep gpRep≤SubR

(SuperClass Rep(trans≤ gpRep≤SubR

gpSubR≤SuperR)[ ops = co sig self .ops,

prfs = co spec self .prfs ])self )

: (Class SuperR SuperSig SuperSpec) →(∀ Rep : ? . (Rep ≤ SubR) →[ops : SuperSig Rep, prfs : SuperSpec Rep ops] →[ops : SubSig Rep, prfs : SubSpec Rep ops] →[ops : SubSig Rep, prfs : SubSpec Rep ops]) →

(Class SubR SubSig SubSpec)

Continuing the example, we use inheritance to constructa class of colored points. Thus assume a type Color : ?together with elements blue, red, . . . . In addition to theoperations getX , setX , and inc1 of points, the class ofcolored points contains the operations inc2 and getC,where the operation inc2 increments the coordinate bytwo and getC extracts the color.

Example 6 Colored points. The signature of coloredpoints SigCPoint extends the signature of points SigPointby the types of the operations inc2 and getC, abstractedover a representation type Rep:

SigCPointdef= λ Rep : ? . [ opspoint : SigPoint Rep,

inc2 : Rep → Rep,getC : Rep → Color ]

To simplify the further exposition, we pretend that theoperations form a flat quintuple. We also use names suchas getX, setX, etc., for the appropriate record selectors,when the meaning is clear from the context.

For the specification SpecCPoint, assume an arbi-trary representation type Rep and operations ops of typeSigCPoint Rep. The specification SpecCPoint extends thespecification SpecPoint by three equations.

SpecCPointdef=

(SpecPoint Rep ops.opspoint) ×( ops.getX (ops.inc2 r) =L (ops.getX r) + 2

ops.getC (ops.inc2 r) =L blueops.getC (ops.setX r n) =L blue )

As in the case of the operations, we assume that theproofs form a flat quintuple. We refer to the compo-nents of prfs which has type SpecCPoint Rep ops by prfs.1through prfs.5.

newdef= λ class : Class ClassR Sig Spec′ .

λ state : ClassR .λ opsbasis : Sig ClassR .λ prfsbasis : Spec′ ClassR opsbasis opsbasis .λ n : nat .let codeprfs = class ClassR (refl≤ ClassR)

operations = nat iter opsbasis codeprfs.code nin λ coderesolved : codeprfs.code operations =L operations .

let proofs = new aux opsbasis prfsbasis n coderesolvedin (ObjectIntro state operations proofs)

: Object Sig Spec

FIG. 1. Instantiation.


Now, we define a class MyCPointClass with represen-tation type (nat × Color) by means of the inheritance op-erator inherit.

MyCPointClassdef=

inherit (nat × Color) SigCPoint SpecCPointgp co sig co specMyPointClass( λ Rep : ? .

λ gpRep≤(nat × Color) : Rep ≤ (nat × Color) .λ super : [ ops : SigPoint Rep,

prfs : SpecPoint Rep ops ].λ self : [ ops : SigCPoint Rep,

prfs : SpecCPoint Rep ops ].[ ops = opsCPointClass,

prfs = prfsCPointClass ]) : Class (nat × Color) SigCPoint SpecCPoint

The term gp : (nat × Color) ≤ nat is a dependent tripleconsisting of functions get = λnc : (nat × Color) . nc.1and put = λnc : (nat × Color) . λn : nat . (n, nc.2) to-gether with the straightforward verification of the re-quired laws. The proof uses the η-rule for pairs whichis provided by their inductive definition from the Lego-library. The coercion co sig : ∀ Rep | ? . SigCPoint Rep→ SigPoint Rep for the signature and co spec of type∀ Rep | ? . ∀ ops | (SigCPoint Rep). (SpecCPoint Rep ops)→ (SpecPoint Rep (co sig ops)) for the specification partrespectively simply forget the new operations and the newproofs.

To implement the operations opsCPointClass, we in-herit getX and inc1 from the superclass of points. Toillustrate late binding, the operation setX of the coloredpoint class artificially sets the color to blue. The opera-tion inc2 uses the operation inc1 of the point-class twiceand getC simply extracts the color. In the definition of theoperations, the variables self and super provide accessto the methods of the colored point class and the pointclass respectively.

opsCPointClass =[ getX = λr : Rep . super.ops.getX r,

setX = λr : Rep . λn : nat .gpRep≤(nat × Color).put r (n, blue),

inc1 = λr : Rep . super.ops.inc1 r,inc2 = λr : Rep . super.ops.inc1

(super.ops.inc1 r),getC = λr : Rep . (gpRep≤(nat × Color).get r).2 ) ]

Finally, we have to prove the correctness of these fiveoperations, i.e., give an element prfsCPointClass of typeSpecCPoint Rep opsCPointClass.

We have to postpone the discussion of the first andthe fourth equation since at this stage it is not possibleto prove propositions relating the variable super withget and put. The problem is similar to the one for selfencountered in the encoding of classes (cf. the Example

on Generalized specification of points above) and will beaddressed in the next section.

The second equation of the quintuple SpecCPointabove reduces to super.ops.getX (super.ops.inc1 r) =L

(super.ops.getX r) + 1, which coincides with the type ofsuper.prfs.2. Therefore, we can use the inherited proofsuper.prfs.2 to show the correctness of the current equa-tion. This equation demonstrates that it is possible toinherit correctness proofs to verify inherited operations.Note that the situation of the previous equation is not assimple as the proof might suggest. The operation inc1 inthe subclass refers, as in the superclass, via self to thesetX operation, which we have changed in the subclass.Due to late binding, this also affects the implementationof inc1. Nevertheless, the inheritance of the proof works,since we have not altered the behavior of setX on thepoint part.

This way of reasoning is not restricted to situationswhere the inherited proof is reused without modification.New equations of a subclass can also be proven by proofinheritance, as can be seen in the third equation.

Expanding the definitions of the operations getXand inc2 in opsCPointClass, the third equation be-comes super.ops.getX (super.ops.inc1 (super.ops.inc1 r))=L (super.ops.getX r) + 2 and can be shown by employ-ing the inherited proof super.prfs.2 twice.

The last equation can be established easily with thelaws for get and put, even though the point part of setXis inherited and in the equation super is mixed with getand put. This is feasible because the definition of thepoint part is irrelevant for the proof.

3. Proofs Over Self-Methods

In this section we improve the encoding of classes, in-stantiation, and inheritance, to overcome the difficultieswith proofs over methods with late binding. The defi-nitions of objects, generic methods, and generic proofmethods remain unchanged.

3.1. Classes

As seen in the previous section, we can cope withequations about non late binding methods. We have alsomentioned in the Example on Generalized specificationof points that some equations with self methods are prov-able, namely if the specification of the self methods suf-fices to establish the properties to be shown. In manycases, especially when self methods appear together withnon-self methods, we are stuck. The reason is that, bylate binding, the self methods may refer to operationsof subclasses whereas the non-self methods refer to thespecial implementation of the present class. For instance,in the Example on Generalized specification of points wecannot expect to prove the second equation in the spec-


ification of points, relating the implementations of getXand inc1:

gp.get (self.ops.setX r (self.ops.getX r) + 1)=L (gp.get r) + 1 (1)

since we do not know how the setX method in subclasseswill behave together with the current implementationgp.get of the getX method. The only thing we knowabout the self-operations is that they satisfy the speci-fication; the verification cannot rely on any details of theimplementation.

In [24] the problem was overcome by including imple-mentation details into the specification.4 In our example,one would then add the equation ops.getX =L gp.get tothe specification of points. This would give the desiredconnection between self and the present implementation:self.ops.getX =L gp.get. However, such a specification ofinternal details is problematic since it also fixes the im-plementation for the subclasses, which will have to sat-isfy the extended specification, too. Even worse: includ-ing implementation details into the objects’ interfacesmisses the point of encapsulation, whose purpose is toabstract away from details.

The previous analysis shows that without restrictionon the implementation of the subclasses equation (1) issimply not true in the class PointClass. Nevertheless, af-ter solving the self-operations of the point class by afixed point, the equation does become provable. The op-erations self.ops.getX and self.ops.setX then get replacedby their implementation, yielding:

gp.get︸︷︷︸

getX

(gp.put︸︷︷︸

setX

r (gp.get︸︷︷︸

getX

r) + 1) =L (gp.get︸︷︷︸

getX

r) + 1

This equation follows from the first equation in the speci-fication of points. This observation applies not only to theclass of points itself, but to all of its subclasses: upon in-stantiation, the self gets replaced by the implementationprovided by the respective subclass. The second equationthen takes the form:

impl.getX(impl.setX r (impl.getX r) + 1) =L

(impl.getX r) + 1 (1sc)

where impl.getX and impl.setX are the concrete imple-mentation of the methods getX and setX , thus satisfyingat least the specification of points. Again we can use thefirst equation of SpecPoint for the proof.

These calculations suggest that the problem with theverification of late binding methods (here inc1) is nota genuine one, but rather caused by a limitation of ourapproach. Simply requiring that a class maps correct im-plementations to correct implementations (as was donein the Definition Type of classes above) is not enough toestablish all reasonable and expected properties.

To overcome this problem, we will consider gener-alized specifications which contain two copies of everymethod: one ranging over the actual implementation andthe other over the self parameter. More formally, we con-

sider Spec′ : ∀ Rep . (Sig Rep) → (Sig Rep) → ?. It is thetask of the programmer or verifier to decide which copyof a method is appropriate for the generalized specifica-tion. We will show below that the fixed point of the pro-gram part of a class satisfies the intended diagonalized

specification Specdef= λ ops : (Sig Rep). Spec′ ops ops. In

the sequel we will use primes to refer to a generalizedspecification and use their name without prime for thediagonalized specification.

In the specification of points, the separation of ab-stract and actual implemented operations is done as fol-lows:

Example 7 Generalized specification of points. As-suming a representation type Rep, concrete opera-tions ops, and abstract operations selfops of typeSigPoint Rep, the generalized specification of points isgiven as

SpecPoint′ def=

ops.getX (ops.setX r n) =L nselfops.getX (ops.inc1 r) =L (selfops.getX r) + 1

Notice that SpecPoint =L SpecPoint′ ops ops.

A class will now provide for all Rep ≤ ClassR:

• a self-dependent implementation code : (Sig Rep) →(Sig Rep) of the operations, and

• a proof that Spec′ selfops selfops′ entails the correct-ness of Spec′(code selfops) selfops.

More formally:

Definition Type of classes. Assume a representa-tion type ClassR : ?, a signature Sig : ? → ?, and ageneralized specification Spec′ : ∀ Rep : ? . (Sig Rep) →(Sig Rep) → ?. Let the term Spec stand for the specifica-tion λ Rep : ? . λ ops : (Sig Rep). Spec′ Rep ops ops, whichrepresents the ungeneralized version of Spec′. The typeof classes is then given as:

Classdef= ∀ Rep : ? . (Rep ≤ ClassR) →

[ code : (Sig Rep) → Sig Rep .prfs : ∀ selfops, selfops′ : Sig Rep .

(Spec′ Rep selfops selfops′) →Spec′ Rep (code selfops) selfops ]

Notice that we have now separated the program part andthe specification part of a class into two components.We could have done so in the case of the simple classesas well, but found the mixing of the two using Σ-typesmore perspicuous.

The rest of the section is concerned with adapting in-stantiation and inheritance. Before starting with instan-tiation, we complete the class of points with the newdefinition.

Example 8 Class of points. The type of points andtheir signature remain unchanged. As shown, the orig-inal specification SpecPoint is slightly generalized toSpecPoint′.


The type of point classes with representation typenat, signature SigPoint, and generalized specificationSpecPoint′, is constructed by means of the type construc-tor Class:

PointClassdef= Class nat SigPoint SpecPoint′

The concrete class MyPointClass is again a pair of op-erations and correctness proofs:

MyPointClassdef=

λ Rep : ? . λ gp : Rep ≤ nat .[code = codePointClass, prfs = prfsPointClass]

: PointClass .

As programs and proofs are now separated, the self ref-erence to the operations and the proofs is no longerachieved by the single variable self , but by two distinctvariables: selfops and selfprfs. The implementation of theoperations can be used without change:

codePointClass =λ selfops : SigPoint Rep .

[ getX = λr : Rep . gp.get r,setX = λr : Rep . λn : nat . gp.put r n,inc1 = λr : Rep . selfops.setX r

(selfops.getX r) + 1 ]

Finally, we have to prove their correctness, i.e., as-suming selfops and selfops′ of type SigPoint Rep andselfprfs of type SpecPoint Rep selfops selfops′, providea correctness proof prfsPointClass of the specificationSpecPoint′ Rep (codePointClass selfops) selfops. Theproof of its first equation is identical to the one in theold definition of this class. The second equation, the onewe had to modify, now β-reduces to

selfops.getX(selfops.setX r (selfops.getX r) + 1) =L

(selfops.getX r) + 1

The self-proof selfprfs.1 : ∀r : Rep . ∀n : nat . selfops.getX(selfops.setX r n) =L n establishes its correctness.

3.2. Instantiation

Next we adapt the instantiation function to deal withthe modified definition of classes. Compared with thedefinition of new in Section 2 the major difference arisesfrom the way the self-dependencies are resolved. In Sec-tion 2 the self-dependent operations and proofs of classesare of the following form:

[ops : Sig Rep, prfs : Spec Rep ops] →[ops : Sig Rep, prfs : Spec Rep ops]

In the setting of Section 2, the fixed point reached byiterating a class yielded both the desired final implemen-tation and its correctness proof. In the present situationwe will iterate the function code : (Sig Rep) → Sig Rep toobtain the final implementation and afterwards construct

its correctness proof using the proof component of theclass. More formally, we proceed as follows.

Suppose that we are given a class of typeClass ClassR Sig Spec′. Applying it to ClassR and to(refl≤ ClassR) and projecting out the components yieldstwo functions:

code : (Sig Rep) → Sig Repprfs : ∀ selfops, selfops′ : Sig Rep .

(Spec′ Rep selfops selfops′) →Spec′ Rep (code selfops) selfops ]

As before, we assume that our specification isconsistent. That is, we assume opsbasis : Sig ClassRand prfsbasis : Spec′ ClassR opsbasis opsbasis. If, as as-sumed, there are no circular self-dependencies in thedefinition of code then there exists a natural numbern such that — starting with opsbasis — after n it-erations a fixed-point of the self-dependent operationscode has been reached, i.e., (code (coden opsbasis)) =(coden opsbasis). Unlike in the setting of Section 2 wenow have to explicitly require a proof coderesolved thatthe fixpoint has been reached after n iterations. Then the(n + 1)-th iteration of the self-dependent proofs (start-ing with prfsbasis : Spec′ Rep opsbasis opsbasis) has typeSpec′ Rep (coden+1 opsbasis) (coden opsbasis) which co-incides with Spec′ Rep (coden opsbasis) (coden opsbasis).Hence the fixed-point of the operations satisfies the spec-ification Spec′. If the iteration index n is such that afterβ-reduction both the n-fold iteration of code and the(n + 1)-fold iteration of prfs do not contain the assump-tions opsbasis and prfsbasis, respectively, then, as in Sec-tion 2, these are no longer needed.

Again, the task of finding such an index n could becarried out by a semi-algorithm which performs a bruteforce search or alternatively by a static analysis of thepossible calls to self .

Definition Instantiation. Assume implicitly a rep-resentation type ClassR, a signature Sig, and a gener-alized specification Spec′. Let the term Spec stand forthe corresponding ungeneralized specification λ Rep : ? .λ ops : (Sig Rep). Spec′ Rep ops ops . The instantiationoperator is thus defined in Figure 1.

The function new aux performs the abovementionediteration of codeprfs.prfs, yielding an element of typeSpec′ ClassR operations operations.

Example 9 Instance of points. The instantiation forpoints remains basically unchanged. Again, only twoiterations are needed to resolve the self-dependencies.Having reached the fixed point of code, the proofcoderesolved is trivial by reflexivity of Leibniz’s equality.

3.3. Inheritance

The last definition to align is the one for inheritance.The basic mechanisms remain unchanged, but the encod-ing now has to deal separately with the operations and


the proofs. We also solve the problem of mixing inheritedoperations with newly implemented ones, encountered inthe Example on Colored points. The problem resemblesthe one that led to the redefinition of classes: there is noconnection between the variable superops, denoting theoperations of the superclass, and the newly implementedoperations. The solution, though, is simpler than the onefor self , since superops stands for an already existingimplementation. In the function build, we simply haveto make available the fact that superops really stands forthe operations of the superclass.

Definition Inheritance. Assume implicitly a rep-resentation type SuperR, a signature SuperSig, and ageneralized specification SuperSpec′ of type ∀ Rep : ? .(SuperSig Rep) → (SuperSig Rep) → ?. Assume a rep-resentation type SubR, a signature SubSig, and a gen-eralized specification SubSpec′ for the subclass. Let theterms SuperSpec and SubSpec denote the ungeneralizedspecifications as in the Definition of classes with general-ized specifications, Type of classes above. Finally assumea proof gpSubR≤SuperR : SubR ≤ SuperR and coercionsco sig of type ∀ Rep | ? . (SubSig Rep) → (SuperSig Rep)and co spec of type

∀ Rep | ? . ∀ selfops, selfops′ | (SubSig Rep).(SubSpec′ Rep selfops selfops′) →

(SuperSpec′ Rep (co sig selfops) (co sig selfops′)

for the operations and proofs respectively. The inheri-tance operator inherit is defined in Figure 2.

The reader should not be discouraged by the sheersize of this term. As can be seen from the Example onColored points, the programmer does not have to bother

about the concrete definition of inherit in a concrete ap-plication.

As far as the readability of the programs is concerned,you have to remember that our programming languageis rigorously encoded within a theorem prover. To makethe language practically more useful, syntactic sugar anda number of special tactics are inevitable. See [45] forsuggestions, how to make the encoding look like a gen-eralized object-oriented programming language.

Continuing with the running example of coloredpoints, the definitions of CPoint, SigCPoint, andSpecPoint from Section 2.3.2. go unchanged, we onlyneed a generalized specification SpecCPoint′.

Example 10 Colored points. For the generalized spec-ification SpecCPoint′, assume an arbitrary representa-tion type Rep, concrete operations ops, and abstract op-erations selfops of type SigCPoint Rep.

SpecCPoint′ def=

( SpecPoint′ Rep ops.opspoint selfops.opspoint ) ×( selfops.getX (ops.inc2 r) =L (selfops.getX r) + 2

selfops.getC (ops.inc2 r) =L blueops.getC (ops.setX r n) =L blue )

Now we can define a class MyCPointClass with represen-tation type (nat × Color) by means of the inheritance op-erator inherit. For the definition of gp : (nat × Color) ≤nat we refer to the Example on Colored points. The twoterms co sig and co spec denote the natural coercion

inheritdef= λ SuperClass : Class SuperR SuperSig SuperSpec′ .

λ build : ∀ Rep : ? . ∀ gpRep≤SubR : Rep ≤ SubR .let gpRep≤SuperR = trans≤ gpRep≤SubR gpSubR≤SuperR

super = SuperClass Rep gpRep≤SuperRin [ code : (SuperSig Rep) → (SubSig Rep) → SubSig Rep,

prfs : ∀ selfops, selfops′ : SubSig Rep .let superops =L super.code (co sig selfops))in (SuperSpec′ Rep superops (co sig selfops)) →

(SubSpec′ Rep selfops selfops′) →SubSpec′ Rep (code superops selfops) selfops ]

( λ Rep : ? . λ gpRep≤SubR : Rep ≤ SubR .let gpRep≤SuperR = trans≤ gpRep≤SubR gpSubR≤SuperR

super = SuperClass Rep gpRep≤SuperRcodeprfs = build Rep gpRep≤SubR

in [ code = λ selfops : SubSig Rep . codeprfs.code (super.code (co sig selfops)) selfops,prfs = λ selfops, selfops′ : SubSig Rep .

λ selfprfs : SubSpec′ Rep selfops selfops′ .codeprfs.prfs selfops selfops′

(super.prfs (co sig selfops) (co sig selfops′)(co spec selfprfs))selfprfs ]

) : Class SubR SubSig SubSpec′

FIG. 2. Inheritance.


functions from colored points to points.

MyCPointClassdef=

inherit (nat × Color) SigCPoint SpecCPoint′gp co sig co specPointClass( λ Rep : ? .

λ gpRep≤(nat × Color) : Rep ≤ (nat × Color) .[ code = codeCPointClass,

prfs = prfsCPointClass ] ): Class (nat × Color) SigCPoint SpecCPoint′

The implementation of the operations is given by thequintuple opsCPointClass.

codeCPointClass =λ superops : SigPoint Rep .λ selfops : SigCPoint Rep .[ getX = λr : Rep . superops.getX r,

setX = λr : Rep . λn : nat .gpRep≤(nat × Color).put r (n, blue),

inc1 = λr : Rep . superops.inc1 r,inc2 = λr : Rep . superops.inc1 (selfops.inc1 r),getC = λr : Rep . (gpRep≤(nat × Color).get r).2 ]

With the modified encoding, all equations of the col-ored point class become provable. Assuming opera-tions selfops, selfops′ : SigCPoint Rep of the subclass, theproofs superprfs of the superclass and the self proofs ofcolored points selfprfs, we have to give a correctnessproof for the specification relatively to the operations justdefined. In the following, we abbreviate the operations ofcolored points as Cops.

Since the setX operation has been reimplemented forcolored points, the inherited proof of the first equationof the point class is of no use for proving the respectiveequation Cops.getX(Cops.setX r n) =L Cops.getX r of thecolored points. This equation β-reduces to:

(gpRep≤(nat × Color).get(gpRep≤(nat × Color).put r (n, blue))).1 =L n

This is immediate by the laws for get and put.The new encoding with the generalized specifications

still admits inheriting proofs for equations containingonly inherited methods. So the proof for the second equa-tion can instantly be obtained by superprfs .2, as in theExample on Colored points.

The third equation can be proved by applyingsuperprfs .1 twice. This example demonstrates that sev-eral references to the proofs of the superclass might beneeded to establish one single equation in the subclass.

The fourth equation selfops.getC (Cops.inc2 r) =L

blue expands into

selfops.getC(selfops.setX (selfops.inc1 r)

((selfops.getX (selfops.inc1 r)) + 1))=L blue

Specialising the proof selfprfs .5 to r = selfops.inc1 r andn = (selfops.getX (selfops.inc1 r))+1 shows that the left-hand side equals blue.

The last equation Cops.getC(Cops.setX r n) =L bluefinally, containing only new methods or reimplementedones, can be proven directly using the implementation ofthe colored point class.

3.4. A More Flexible Definition of Classes

We have also experimented with the followingweaker, i.e., easier to implement, definition of classes:

Class′ def= ∀ Rep : ? . (Rep ≤ ClassR) →

[ code : (Sig Rep) → Sig Rep .prfs : ∀ selfops : Sig Rep .

(Spec′ Rep selfops selfops) →Spec′ Rep (code selfops) selfops ]

As before, let operations stand for the fixpointof code obtained by an appropriate number of it-erations. Now, in order to obtain an element ofSpec′ ClassR operations operations by iterating prfswe need to start with variable prfsbasis of typeSpec′ ClassR operations operations, so it seems as ifnothing has been gained. If, however, it so happens thatthe assumed variable drops out after a certain number ofiterations then, again, we have shown the correctness ofoperations without assumptions.

So, in this case, β-reduction on proofs is really re-quired for the soundness of the formalism.

Our experience is that the definition Class′ is moreflexible in case references to both self and super are madein the definition of one and the same method. For exam-ple, if we implement inc2 in the Example of coloredpoints as

inc2 = superops.inc1 (selfops.inc1 r),

then in the formerly presented formalism a verification ispossible only if we would include certain implementationdetails into the specification, whereas in the “alternative”one it goes through immediately without changes.

We find this essential use of β-reduction on proofs in-teresting and worth exploring but need more experienceto gauge its possible merits and drawbacks.

4. Conclusion and Further Work

Building upon the object-model of Pierce, Turner, andHofmann ([48] [24]), this paper has presented a wayto integrate formal verification into an object-orientedprogramming language. By augmenting the interface ofobjects by a specification of behavior, we have demon-strated that object-oriented structuring techniques can beemployed in organizing proofs as well. Our experience sofar has been that these object-oriented structuring tech-niques allow for flexible reuse of proofs. However, we


have to concede that more substantial examples are re-quired to justify this.

A first step in this direction is the case study con-cerned with Smalltalk-style collections contained in [44].In this case study we noticed that abstract classes, i.e.,classes not meant to be instantiated into objects, are anatural mechanism to reduce the verification effort. Inour setting, abstract classes are classes that contain meth-ods or proofs referring to themselves via the variable selfand which we call abstract methods or abstract proofs.Note that abstract classes do not denote a new concept,but refer to a special usage of the already encounteredmechanism of self-reference.

To understand how abstract classes allow flexiblereuse of methods, consider a class Root as root of thehierarchy of collection classes, which provides methodscommon to all collections. Let us just focus on four op-erations, common to all collections: length, add, empty,and fold, with the usual meaning. In the class Root, thethree methods fold, add, and empty are abstract, i.e.,fold = self.fold, add = self.add, empty = self.empty, andthe fourth method length is defined straightforwardly interms of fold. No matter which implementation of foldwe will eventually choose in a subclass, the correspond-ing length will always be defined.

An analogous mechanism — abstract proofs — sup-ports flexible reuse of proofs. Consider the following in-duction principle:

(P empty) → (∀a, c.(P c) → (P (add a c))) → ∀c.(P c)

In the root class Root we cannot provide a proof ofsuch an induction principle yet, since empty and addare merely abstract. Instead of proving this rule directly,we introduce an abstract proof defined as induction =self.induction. Using this not yet proven induction prin-ciple we can prove properties about the class Root whichcan be inherited by concrete subclasses. The mechanismof proof inheritance takes care that the proofs relyingon it are adapted automatically in subclasses, depend-ing on the specific implementation of the representationtype, on the chosen operations, and on their correctnessproofs (including the deferred proof of the inductionprinciple for the concrete representations of non-abstractsubclasses).

Comparison with Other Work

In Lego much work has been done in formalizingmathematical theories and also in the field of programspecification and verification [35] [8] [51] [23] [51] [55],to mention several. Whilst there is an increasing body ofwork about the semantic foundations of object-orientedprogramming, notably in the area of typed functional cal-culi (see, for example, [21] for a collection of relevant

papers), there are still only a few investigations about theverification of specifically object-oriented programs.

Leavens and Weihl in a series of papers [28, 29, 30,32, 31] investigate modular specification and verificationof object-oriented programs featuring subtype polymor-phism and late-binding. Modular verification in their set-ting means: adding a new type to a program must notcall for recoding, respecification, or reverification of oldmodules. In the presence of subtyping, the aim is to usethe proofs for objects of the supertype also for objectsof all subtypes without change. The problem with latebinding methods for verification is that on the one handone wishes a “static” verification of properties for ob-jects of a given class, but on the other hand inheritanceand late-binding of methods can lead to a different se-mantics in subsequent subclasses. The solution presentedis to separate the implementation from its abstract rep-resentation, to assign a static type to the objects as upperbound (its nominal type), and use the abstract specifica-tion to reason about objects of all of its subtypes. Thusobjects of a smaller type must not only accept messagesmeant for objects of a larger type without “message notunderstood” run-time error, but in addition they have toexhibit the same behavior, as given in the interface spec-ification. Since structural subtyping — employed, e.g.,in F ω≤’s (sub-)type system — is too weak to accountfor compliance with specifications, the notion of subtyp-ing needs a refinement; this stronger notion of behavior-preserving subtyping is known as behavioral subtyping[2]. To obtain a convenient mathematical model of theabstractly specified objects, they restrict their attentionto objects with immutable state which can be modelledas abstract data types. Hoare style specification is usedto specify the behavior of the objects via so-called traitsin the Larch interface specification language as pre- andpost-condition of the object’s methods. An extension totypes with mutable state and aliasing, in an algebraicframework, is presented in [15]. Sticking to an algebraicframework, though, in the presence of a mutable stateseems to complicate the model considerably.

In contrast to the work of Leavens and Weihl, Ut-ting [53] [54] handles objects with mutable state, but atthe expense of data refinement, i.e., in the refinementprocess, inheritance may not change the internal repre-sentation of objects. A methodological difference is thathe favors program development by a series of transfor-mations. To this end an extension of refinement calculusof [4] [42] [41], being itself an extension of Dijkstra’sguarded command language [16], is presented, a widespectrum language, where executable code and specifi-cations can be freely mixed.

Further Work

Apart from the need for developing more extensivecase studies, several directions for further work suggest


themselves. Our approach is based on an encoding of onespecific, albeit powerful and well-studied, object model.It would be worthwhile to extend or change the encod-ing to comprise other object-oriented features or idioms,such as multiple inheritance, which can be modelled in anextension of F ω≤ with intersection types [11]. One couldadd syntactic sugar or fancier notions of specification,e.g., splitting the specification into a visible, externalpart, and an internal, hidden one.

A pragmatic path might be, to spare the user from per-forming every minute step of the required proofs. Thiscould include the automatic generation of the get and putfunctions proposed in [24] for positive signatures, or theautomatic calculation of the number of fixpoint unwind-ings. To perform larger case studies, a high-level syntaxis inevitable that withholds Lego–specific notations andcommands.

Besides verifying properties of actual programs, thetransfer into Lego could also be used to prove generalproperties about the encoding itself, such as propertiesof the inheritance or instantiation operator.

A deeper question concerns the equality of objects. Anintensional equality such as Leibniz’s equality is inade-quate for the comparison of objects, since it would dis-tinguish between objects of different implementations,which contradicts the idea of encapsulation. As pointedout in Section 2.3.3., it is also problematic to place thetest of equality on objects as an equality method insidethe objects. In the chosen model, generic methods can-not be defined for signatures containing binary genericmethods like a method comparing two objects whose in-ternal representation is hidden by weak existential quan-tification. We believe that the correct equality for ob-jects would be given by observational equivalence withrespect to method invocations as advocated, e.g., by Ja-cobs [26].

Acknowledgments

Many thanks to Luis Dominguez, Michael Mendler,and Uwe Nestmann for giving useful suggestions on ear-lier versions which helped to improve the paper. We aregrateful to the members of the Lego-club at the LFCSwhose comments influenced the entire work. In partic-ular we want to thank Rod Burstall, James McKinna,and Thomas Schreiber for their discussions. Finally wethank the two anonymous referees for their helpful re-marks and Benjamin Pierce for his suggestions for thefinal version.

This research was supported by the Spezifikation undVerifikation verteilter Systeme project, funded by theDeutsche Forschungsgemeinschaft, Sonderforschungs-bereich 182, and by the British Council and theDeutscher Akademischer Austauschdienst within the

ARC-programme “Ko-Entwicklung objektorientierterProgramme in Lego.”

Notes

1. In this work, the higher universes are not used and instead weemploy the impredicative universe ? for both propositions anddatatypes. Since we don’t make use of the hierarchy of universes,our development could be realized in the Calculus of Constructionswith inductive types as implemented in the Coq system [13], too.We wish to stress that the use of a single universe for both propo-sitions and types is | although pragmatically advantageous | notcrucial for our approach. It would work equally well if we wouldemploy two impredicative universes Set and ? like in the Coqsystem. It seems plausible that the program extraction mechanismof Coq which strips off all terms of kind ? from a type-theoreticdevelopment could be extended to object-oriented programs. Thedrawback of having two separated universes is that we would haveto duplicate various definitions and rules and also that the Legoimplementation does not provide Set and ?.

2. The Lego-sources can be accessed by anonymous ftp atftp.informatik.uni-erlangen.de in the directory /lo-cal/ inf7/vs/sfbc2/lego/oo-verification.l

3. The intensional notion of Leibnitz’s equality equates elements ofthe same type if they cannot be distinguished by any predicate overthis type.

4. An extension to the encoding presented so far to specify suchdetails has been presented in [43], using ideas of [24].

References

[1] ACM (1990). Seventeenth Annual Symposium on Principles of Pro-gramming Languages (POPL), January 1990.

[2] America, P. (1989). A behavioural approach to subtyping in object-oriented programming languages, 443, Phillips Research Labora-tories, January/April 1989.

[3] Audebaud, P. (1993). CC+: An extension of the Calculus of Con-structions with fixpoints. Research Report 93-12, Laboratoire del’Informatique du Parallelisme, Ecole Normale Superieure deLyon Unite de recherche associee au CNRS, July 1993.

[4] Back, R.-J. R. (1978). On the Correctness of Refinement in Pro-gram Development. Ph.D. Thesis, Department of Computer Sci-ence, University of Helsinki.

[5] Barendregt, H. P. (1992). Lambda calculi with types. In: SamsonAbramsky, Dov Gabbay, and Thomas Maibaum, eds., Handbookof Logic in Computer Science, Vol. 1, Mathematical Structures,pp. 117–309. Oxford University Press, 1992.

[6] Bruce, K. B. (1994). A paradigmatic object-oriented programminglanguage: Design, static typing and semantics, J. Funct. Program-ming, 4(2). a preliminary version appeared in POPL 1993 underthe title Safe type checking in a statically typed object-orientedprogramming language, and as Williams College Technical Re-port CS-92-01.

[7] Bruce, K. B., Cardelli, L., Castagna, G., the Hopkins ObjectsGroup (Eifrig, J., Smith, S., Trifonov, V.), Leavens, G. T., andPierce, B. (1996). On binary methods, Theo. Prac. Obj. Syst.,1(3):221–242.

[8] Burstall, R., and McKinna, J. (1993). Deliverables: a categori-cal approach to program development in type theory. In: A. M.Borzyszkowski and S. Sokołowski, eds., Eighteenth Mathemati-cal Foundations of Computer Science (Gdansk, Poland), LectureNotes in Computer Science, Vol. 711, pp. 32–67, Springer-Verlag.

[9] Cardelli, L. (1997). Type systems. In: Allen B. Tucker, ed., Hand-book of Computer Science and Engineering, Chapter 103, CRCPress.

[10] Cardelli, L., and Wegner, P. (1985). On understanding types, dataabstraction and polymorphism, Comput. Surveys, 17(4):471–522.


[11] Compagnoni, A. B., and Pierce, B. C. (1996). Intersection typesand multiple inheritance, Math. Structures Comput. Sci., 6(5):469–501. A preliminary version available as University of EdinburghTechnical Report ECS-LFCS-93-275 and Catholic University Ni-jmegen Computer Science Technical Report 93-18, August 1993,under the title Multiple Inheritance via Intersection Types.

[12] Cook, W. R., Hill, W. L., and Canning, P. S. (1990). Inheritance isnot subtyping. In: Seventeenth Annual Symposium on Principles ofProgramming Languages (POPL) (San Fancisco, CA) [1], pp. 125–135. Also in the collection [21].

[13] Cornes, C., Courant, J., Filiatre, J.-C., Huet, G., Manoury, P.,Mounoz, C., Murthy, C., Parent, C., Paulin-Mohring, C., Saıbi,A., and Werner, B. (1995). The Coq Proof Assistant User’s Guide.Rapports Techniques 0177, INRIA Rocquencourt, Projet Formel.Version 5.10.

[14] Curien, P.-L., and Ghelli, G. (1990). Coherence of Subsumption.Technical Report LIENS 90-10, Laboratoire d’Informatique del’Ecole Normale Superieure.

[15] Dhara, K. K., and Leavens, G. T. (1992). Subtyping for Muta-ble Types in Object-Oriented Programming Languages. TechnicalReport, Iowa State University, Department of Computer Science,November 1992, TR 92-36, submitted to ECOOP ’93.

[16] Dijkstra, E. W. (1976). A Discipline of Programming. PrenticeHall.

[17] Fisher, K. (1996). Type Systems for Object-Oriented Languages.Ph.D. Thesis, Stanford University.

[18] Fisher, K., and Mitchell, J. (1996). The development of type systemsfor object-oriented languages, Theo. Prac. Obj. Syst., 1(3):189–220. An earlier version appeared in [22] under the title Notes onTyped Object-Oriented Programming.

[19] Girard, J.-Y. (1972). Interpretation fonctionelle et elimination descoupure dans l’arithmetique d’ordre superieur. Ph.D. Thesis, Uni-versite Paris VII.

[20] Goldberg, A., and Robson, D. (1983). Smalltalk-80: The Languageand Its Implemementation. Addison-Wesley, Reading, MA.

[21] Gunter, C. A., and Mitchell, J. C. (1994). Theoretical Aspects ofObject-Oriented Programming, Types, Semantics, and LanguageDesign. Foundations of Computing Series. MIT Press.

[22] Hagiya, M., and Mitchell, J. C., eds. (1994). Theoretical Aspectsof Computer Software, Lecture Notes in Computer Science, Vol.789, Springer-Verlag.

[23] Hofmann, M. (1992). Formal Development of Functional Pro-grams in Type Theory — A Case Study. Report ECS-LFCS-92-228,Laboratory for Foundations of Computer Science, University ofEdinburgh.

[24] Hofmann, M., and Pierce, B. (1994). Positive subtyping. In:Twenty-Second Annual Symposium on Principles of Program-ming Languages (POPL) (San Francisco, California), pp. 186–197,ACM, Full version in Inform. and Comput., Vol. 126, No. 1, April1996. Also available as University of Edinburgh Technical ReportECS-LFCS-94-303, September 1994.

[25] Hofmann, M., and Pierce, B. (1995). A unifying type-theoreticframework for objects, J. Funct. Programming, 5(4):593–635. Pre-vious versions appeared in the Symposium on Theoretical Aspectsof Computer Science, 1994, pp. 251–262, and, under the title AnAbstract View of Objects and Subtyping (Preliminary Report), asUniversity of Edinburgh, LFCS Technical Report ECS-LFCS-92-226, 1992.

[26] Jacobs, B. (1996). Objects and classes, coalgebraically. In: C. B.Jones, C. Lengauer, and H.-J. Schek, eds., Object-Orientation withParallelism and Persistence. Kluwer.

[27] Jones, C., and Maharaj, S. (1994). The lego Library. Availableon the World Wide Web [33].

[28] Leavens, G. T. (1988). Verifying Object-Oriented Programs thatUse Subtypes. Ph.D. Thesis, Massachusetts Institute of Technol-ogy.

[29] Leavens, G. T. (1990). Modular Verification of Object-OrientedPrograms with Subtypes. Technical Report 90-09, Iowa State Uni-versity, Department of Computer Science.

[30] Leavens, G. T. (1991). Specifying and Verifying Object-OrientedPrograms: An Overview of the Problems and a Solution. TechnicalReport, Iowa State University, Department of Computer Science.

[31] Leavens, G. T. (1993). Inheritance of Interface Specifications.Technical Report TR 93-23, Iowa State University, Departmentof Computer Science, (Extended Abstract).

[32] Leavens, G. T., and Wheil, W. E. (1994). Specification and veri-fication of object-oriented programs using supertype abstraction,Acta Inform. An expanded version appeared as Iowa State Uni-versity Report, 92-28d.

[33] The lego World Wide Web page (1997). Accessible electroni-cally through http://www.dcs.ed.ac.uk/home/lego.

[34] Luo, Z. (1990). An Extended Calculus of Constructions. ThesisECS-LFCS-90-118, Laboratory for Foundations of Computer Sci-ence, University of Edinburgh.

[35] Luo, Z. (1992). A Unifying Theory of Dependent Types: TheSchematic Approach. Technical Report ECS-LFCS-92-202, Labo-ratory for Foundations of Computer Science, University of Edin-burgh.

[36] Luo, Z., and Pollack, R. (1992). Lego Proof Development System:User’s Manual. Technical Report ECS-LFCS-92-211, Laboratoryfor Foundations of Computer Science, University of Edinburgh.

[37] MacQueen, D. (1986). Using dependent types to express modularstructure. In: Thirteenth Annual Symposium on Principles of Pro-gramming Languages (POPL) (St. Peterburg Beach, FL), pp. 277–286, ACM,

[38] Mitchell, J. C. (1990). Toward a typed foundation for method spe-cialization and inheritance. In: Seventeenth Annual Symposiumon Principles of Programming Languages (POPL) (San Fancisco,CA) [1], pp. 109–124. Also in the collection [21].

[39] Mitchell, J. C. (1996). Foundations of Programming Languages.Foundation of Computing Series, MIT Press.

[40] Mitchell, J. C., and Plotkin, G. D. (1988). Abstract types have ex-istential type, ACM Trans. Programming Languages and Systems,10(3):470–502.

[41] Morgan, C. C. (1990). Programming from Specifications. PrenticeHall.

[42] Morris, J. M. (1987). A theoretical basis for stepwise refine-ment and the programming calculus, Sci. Comput. Programming,9(3):287–306.

[43] Naraschewski, W. (1995). Object-oriented proving. In: Programs& Proofs: Working in Type Theory, Hetzelsdorf, 14–18 August1995.

[44] Naraschewski, W. (1996). Object-Oriented Proof Principles usingthe Proof-Assistant Lego. Diplomarbeit, Universitat Erlangen.

[45] Naraschewski, W. (1997). Towards an object-oriented progi-fication language. In: Proceedings of the 1997 Interna-tional Conference in Theorem Proving in Higher OrderLogics, Bell Labs, Murray Hill, NJ, USA. To appear inSpringer Lecture Notes in Computer Science. Available throughhttp://www4.informatik.tu-muenchen.de/∼narasche/ TPHOL/main.dvi.

[46] Pierce, B. (1993). F-Omega-Sub User’s Manual, Version 1.4,.Available by ftp as part of the fomega implementation.

[47] Pierce, B., and Turner, D. (1992). Object-Oriented Programmingwithout Recursive Types. Technical Report ECS-LFCS-92-225,Laboratory for Foundations of Computer Science, University ofEdinburgh. See also Principles of Programming Languages (POPL’93).

[48] Pierce, B., and Turner, D. (1994). Simple type-theoretic founda-tions for object-oriented programming, J. Funct. Programming,4(2):207–247. A preliminary version appeared in Principles of Pro-gramming Languages, 1993, and as University of Edinburgh Tech-nical Report ECS-LFCS-92-225, under the title Object-OrientedProgramming Without Recursive Types.

[49] Reus, B. (1995). Program Verification in Synthetic Domain Theory.Ph.D. Thesis, Universitat Munchen.


[50] Reynolds, J. (1974). Towards a theory of type structure. In:B. Robinet, ed., Colloque sur la programmation (Paris, France),Lecture Notes in Computer Science, Vol. 19, pp. 408–425,Springer-Verlag.

[51] Schreiber, T. (1993). Verifikation von imperativen Programmen mitdem Beweisprufer Lego. Diplomarbeit, Universitat Erlangen.

[52] Steffen, M., and Pierce, B. (1994). Higher-order subtyping. In:Working Conference on Programming Concepts, Methods and Cal-culi, San Miniato, Italy, pp. 511–530, IFIP, North-Holland. Fullversion in Theoret. Comput. Sci., Vol. 176, Nos. 1–2, pp. 235–282, 1997.

[53] Utting, M. (1992). An Object-Oriented Refinement Calculus withModular Reasoning. Ph.D. Thesis, University of New SouthWales, Australia.

[54] Utting, M., and Robinson, K. (1992). Modular reasoning in anobject-oriented refinement calculus. In: R. S. Bird, C. C. Morgan,and J. P. C. Woodcock, eds., Mathematics of Program Construction1992, Lecture Notes in Computer Science, Vol. 669, pp. 344–367,Springer-Verlag.

[55] Wand, P. (1992). Functional Programming and Verification withLego. Master’s Thesis, Laboratory for Foundations of ComputerScience, University of Edinburgh.


Inheritance of proofs

Documents

Transcript of Inheritance of proofs