Author name cluster

Benjamin C. Pierce

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

1 author row

TCS Journal 2007 Journal Article

A bisimulation for dynamic sealing

Eijiro Sumii
Benjamin C. Pierce

We define λ seal, an untyped call-by-value λ -calculus with primitives for protecting abstract data by sealing, and develop a bisimulation proof method that is sound and complete with respect to contextual equivalence. This provides a formal basis for reasoning about data abstraction in open, dynamic settings where static techniques such as type abstraction and logical relations are not applicable.

Details DOI

I&C Journal 2002 Journal Article

Foundations for Virtual Types

Atsushi Igarashi
Benjamin C. Pierce

Virtual types have been proposed as a notation for generic programming in object-oriented languages—an alternative to the more familiar mechanism of parametric classes. The trade-offs between the two mechanisms are a matter of current debate: for many examples, both appear to offer convenient (indeed almost interchangeable) solutions; in other situations, one or the other seems to be more satisfactory. However, it has proved difficult to draw rigorous comparisons between the two approaches, partly because current proposals for virtual types vary considerably in their details, and partly because the proposals themselves are described rather informally, usually in the complicating context of full-scale language designs. Work on the foundations of object-oriented languages has already established a clear connection between parametric classes and the polymorphic functions found in familiar typed lambda-calculi. Our aim here is to explore a similar connection between virtual types and dependent records. We present, by means of examples, a straightforward model of objects with embedded type fields in a typed lambda-calculus with subtyping, type operators, fixed points, dependent functions, and dependent records with both bounded and manifest type fields (this combination of features can be viewed as a measure of the inherent complexity of virtual types). Using this model, we then discuss some of the major differences between previous proposals and show why some can be checked statically while others require run-time checks. We also investigate how the partial “duality” of virtual types and parametric classes can be understood in terms of translations between universal and (dependent) existential types.

Details DOI

I&C Journal 2002 Journal Article

On Inner Classes

Atsushi Igarashi
Benjamin C. Pierce

Inner classes in object-oriented languages play a role similar to nested function definitions in functional languages, allowing an object to export other objects that have direct access to its own methods and instance variables. However, the similarity is deceptive: a close look at inner classes reveals significant subtleties arising from their interactions with inheritance. The goal of this work is a precise understanding of the essential features of inner classes; our object of study is a fragment of Java with inner classes and inheritance (and almost nothing else). We begin by giving a direct reduction semantics for this language. We then give an alternative semantics by translation into a yet smaller language with only top-level classes, closely following Java's Inner Classes Specification. We prove that the two semantics coincide, in the sense that translation commutes with reduction, and that both are type-safe.

Details DOI

I&C Journal 2002 Journal Article

Type Destructors

Martin Hofmann
Benjamin C. Pierce

We study a variant of System F ≤ that integrates and generalizes several existing proposals for calculi with “structural typing rules. ” To the usual type constructors (→, ×, All, Some, Rec) we add a number of type destructors, each internalizing a useful fact about the subtyping relation. For example, in F ≤ with products every closed subtype of a product S×T must itself be a product S′×T′ with S′<: S and T′<: T. We internalise this observation by introducing type destructors. 1 and. 2 and postulating an equivalence T=ηT. 1×T. 2 whenever T<: U×V (including, for example, when T is a variable). In other words, every subtype of a product type literally is a product type, modulo η-conversion. Adding type destructors provides a clean solution to the problem of polymorphic update without introducing new term formers, new forms of polymorphism, or quantification over type operators. We illustrate this by giving elementary presentations of two well-known encodings of objects, one based on recursive record types and the other based on existential packages. The formulation of type destructors poses some tricky meta-theoretic problems. We discuss two different variants: an “ideal” system where both constructors and destructors appear in general forms, and a more modest system, F ≤ TD, which imposes some restrictions in order to achieve a tractable metatheory. The properties of the latter system are developed in detail.

Details DOI

I&C Journal 2000 Journal Article

Decoding Choice Encodings

Uwe Nestmann
Benjamin C. Pierce

We study two encodings of the asynchronous π-calculus with input-guarded choice into its choice-free fragment. One encoding is divergence-free, but refines the atomic commitment of choice into gradual commitment. The other preserves atomicity, but introduces divergence. The divergent encoding is fully abstract with respect to weak bisimulation, but the more natural divergence-free encoding is not. Instead, we show that it is fully abstract with respect to coupled simulation, a slightly coarser—but still coinductively defined—equivalence that does not enforce bisimilarity of internal branching decisions. The correctness proofs for the two choice encodings introduce a novel proof tech- nique exploiting the properties of explicit decodings from translations to source terms.

Details DOI

I&C Journal 1999 Journal Article

Comparing Object Encodings

Kim B. Bruce
Luca Cardelli
Benjamin C. Pierce

Recent years have seen the development of several foundational models for statically typed object-oriented programming. But despite their intuitive similarity, differences in the technical machinery used to formulate the various proposals have made them difficult to compare. Using the typed lambda-calculus F ω <: as a common basis, we now offer a detailed comparison of four models: (1) a recursive-record encoding similar to the ones used by Cardelli, Reddy, Cook, and others; (2) Hofmann, Pierce, and Turner's existential encoding; (3) Bruce's model based on existential and recursive types; and (4) Abadi, Cardelli, and Viswanathan's type-theoretic encoding of a calculus of primitive objects.

Details DOI

I&C Journal 1996 Journal Article

Positive Subtyping

Martin Hofmann
Benjamin C. Pierce

The statementS⩽Tin aλ-calculus with subtyping is traditionally interpreted by a semantic coercion function of type [[S]]→[lsqb; T]] that extracts the “Tpart” of an element ofS. If the subtyping relation is restricted to covariant positions, this interpretation may be enriched to include both the implicit coercion and an overwriting functionput[S, T]∈[[S]]→[[T]]→[[S]] that updates theTpart of an element ofS. We give a realizability model and a sound equational theory for a second-order calculus of positive subtyping. Though weaker than familiar calculi of bounded quantification, positive subtyping retains 1? sufficient power to model objects, encapsulation, and message passing, and inheritance. The equational laws relating the behavior of coercions andputfunctions can be used to prove simple properties of the resulting? classes in such a way that proofs for superclasses are “inherited” by subclasses.

Details DOI