Mitchell Wand

I&C Journal 1991 Journal Article

Type inference for record concatenation and multiple inheritance

• Mitchell Wand

We show that the type inference problem for a lambda calculus with records, including a record concatenation operator, is decidable. We show that this calculus does not have principal types, but does have finite complete sets of types: that is, for any term M in the calculus, there exists an effectively generable finite set of type schemes such that every typing for M is an instance of one of the schemes in the set. We show how a simple model of object-oriented programming, including hidden instance variables and multiple inheritance, may be coded in this calculus. We conclude that type inference is decidable for object-oriented programs, even with multiple inheritance and classes as first-class values.

I&C Journal 1989 Journal Article

Incorporating static analysis in a combinator-based compiler

• Margaret Montenyohl
• Mitchell Wand

We show how restructuring a denotational definition leads to a more efficient compiling algorithm. Three semantics-preserving transformations (static replacement, factoring, and combinator selection) are used to convert a continuation semantics into a formal description of a semantic analyzer and code generator. The compiling algorithm derived below performs type checking before code generation so that type-checking instructions may be omitted from the target code. The optimized code is proved correct with respect to the original definition of the source language. The proof consists of showing that all transformations preserve the semantics of the source language.

TCS Journal 1982 Journal Article

Specifications, models, and implementations of data abstractions

• Mitchell Wand

We consider the specification and verification of modules in hierarchically structured programs, as proposed by Parnas and Hoare. We argue that a specification for such a module is a set of sentences in some logical language in which the names to be exported by the module appear as nonlogical symbols. We further argue that an implementation of one module in terms of another module is a translation of the nonlogical symbols of the first specification into the language of the second. Equality must also be interpreted. We proposed necessary conditions which any such notion of ‘correct implementation’ ought to satisfy. These criteria provide a basis for judging the logical adequacy of any proposed specification language and definition of implementation. We then study DLP, a specification language obtained by adding uninterpreted procedure symbols to Pratt's first order dynamic logic. We present a definition of ‘implementation’ for DLP, and we show it satisfies these conditions. The main theorem, called the implementation Theorem, extends the Interpretation Theorem from first-order logic to DLP. The proof of this theorem is complicated by the necessity of dealing with modalities, parameters to procedures, interpretations of equality, and interpretations of sorts as tuples.

TCS Journal 1979 Journal Article

Fixed-point constructions in order-enriched categories

• Mitchell Wand

The fixed-point construction of Scott, giving a continuous lattice solution of equations X ≅ T(X) where T is an endofunctor on the category of continuous lattices, is extended to categories enriched by partial orderings on the morphism sets. The result allows data structures to be realized not only in the category of continuous lattices, but also in the category of complete lattices, in the category of complete partial orders, or in any of several related categories of partial orders.

STOC Conference 1976 Conference Paper

A New Incompleteness Result for Hoare's System

• Mitchell Wand

A structure A is presented for which Hoare's formal system for partial correctness is incomplete, even if the entire first-order theory of A is included among the axioms. It follows that the language of first-order logic is insufficient to express all loop invariants. The implications of this result for program-proving are discussed.

STOC Conference 1973 Conference Paper

An Unusual Application of Program-Proving

• Mitchell Wand