Author name cluster

Robert Harper

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.

3 papers

1 author row

TCS Journal 2018 Journal Article

Exception tracking in an open world

Robert Harper

A refinement is a predicate on the elements of a type that describes their execution behavior. Much work has gone into developing refinements in a closed world, in which the classes of values of a type are fixed statically, as in the case of the natural numbers with zero and succ. Relatively little work has gone into developing refinements in an open world in which new classes may be added dynamically. Here we examine the problem of exception tracking, a perennially problematic typing concept for programming languages, from the point of view of refinements in an open world. Exceptions are decomposed into separate control and data mechanisms, the latter motivating the need for open-world refinements. Exception tracking is thereby repositioned as a matter of program verification, rather than structural typing, integrating behavioral typing with theorem proving even in an open world. Some further applications of dynamic classification and open-world refinements are suggested.

Details DOI

TCS Journal 2003 Journal Article

Automated techniques for provably safe mobile code

Christopher Colby
Karl Crary
Robert Harper
Peter Lee
Frank Pfenning

We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary. Concrete realizations of this framework are proof-carrying code, where the evidence for safety is a formal proof generated by a certifying compiler, and typed assembly language, where the evidence for safety is given via type annotations propagated throughout the compilation process in typed intermediate languages. Validity of the evidence is established via a small trusted type checker, either directly on the binary or indirectly on proof representations in a logical framework.

Details DOI

TCS Journal 1991 Journal Article

Type checking with universes

Robert Harper
Robert Pollack

Various formulations of constructive type theories have been proposed to serve as the basis for machine-assisted proof and as a theoretical basis for studying programming languages. Many of these calculi include a cumulative hierarchy of “universes”, each a type of types closed under a collection of type-forming operations. Universes are of interest for a variety of reasons, some philosophical (predicative vs. impredicative type theories), some theoretical (limitations on the closure properties of type theories) and some practical (to achieve some of the advantages of a type of all types without sacrificing consistency.) The Generalized Calculus of Constructions (CCω) is a formal theory of types that includes such a hierarchy of universes. Although essential to the formalization of constructive mathematics, universes are tedious to use in practice, for one is required to make specific choices of universe levels and to ensure that all choices are consistent. In this paper we study several problems associated with type checking in the presence of universes in the context of CCω. First, we consider the basic type checking and well-typedness problems for this calculus. Second, we consider a formulation of Russell and Whitehead's “typical ambiguity” convention whereby universe levels may be elided, provided that some consistent assignment of levels leads to a correct derivation. Third, we consider the introduction of definitions to both the basic calculus and the calculus with typical ambiguity. This extension leads to a notion of “universe polymorphism” analogous to the type polymorphism of ML. Although our study is conducted for CCω, we expect that our methods will apply to other variants of the Calculus of Constructions and to type theories such as Constable's V3.

Details DOI