Skip to main content
PRL Project

Formal Objects in Type Theory Using Very Dependent Types

by Jason Hickey

Foundations of Object-Oriented Languages 3

  • unofficial copies PDF, PS

In this paper we present an extension to basic type theory to allow a uniform construction of abstract data types (ADTs) having many of the properties of objects, including abstraction, subtyping, and inheritance. The extension relies on allowing type dependencies for function types to range over a well-founded domain. Using the propositions-as-types correspondence, abstract data types can be identified with logical theories, and proofs of the theories are the objects that inhabit the corresponding ADT.

bibTex ref: Hic96a

cite link