MIME-Version: 1.0 Server: CERN/3.0 Date: Sunday, 01-Dec-96 20:31:32 GMT Content-Type: text/html Content-Length: 4836 Last-Modified: Thursday, 29-Aug-96 14:38:00 GMT Jason Hickey's Papers at Cornell

Some Cornell Papers


Jason J. Hickey, A Semantics of Objects in Type Theory. Forthcoming Tech Report (also submitted to POPL '97). PostScript file

Here are some formal definitions and theorems for the semantics presented in the paper. These are just the bare formalizations; I plan to provide a guide that makes it easier to walk the proofs.

Abstract: We present a semantics of object calculi in type theory. This interpretation serves to provide a solid mathematical foundation for object-oriented programming. The calculi we consider support self-application, method selection, functional method update, and subtyping with method subsumption. Our interpretation provides this support without the need for recursive types to represent ``Self,'' and it provides a new analysis of objects where the requirements for subsumption are expressed directly in the method types.


Jason J. Hickey, Formal Objects in Type Theory Using Very Dependent Types. PostScript file.

Abstract: 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.

I also have the slides from my talk. PDF slides are better, but if you don't have Acrobat, here are PostScript slides.


John O'Leary, Miriam Leeser, Mark Aagard, and Jason Hickey, Non-Restoring Integer Square Root: A Case Study in Design by Pricipled Optimization. PostScript file.

Abstract: Theorem proving techniques are particularly well suited for reasoning about arithmetic above the bit level and for relating different levels of abstraction. In this paper we show how a non-restoring integer square root algorithm can be transformed to a very efficient hardware implementation. The top level is a Standard ML function that operates on unbounded integers. The bottom level is a structural description of the hardware consisting of an adder/subtracter, simple combinational logic and some registers. Looking at the hardware, it is not at all obvious what function the circuit implements. At the top level, we prove that the algorithm correctly implements the square root function. We then show a series of optimizing transformations that refine the top level algorithm into the hardware implementation. Each transformation can be verified, and in places the transformations are motivated by knowledge about the operands that we can guarantee through verification. By decomposing the verification effort into these transformations, we can show that the hardware design implements a square root. We have implemented the algorithm in hardware both as an Altera programmable device and in full-custom CMOS.


Jason J. Hickey, Formal Abstract Data Types. PostScript file

Abstract: Current constructive type theories are powerful systems for describing mathematical objects with complex dependencies between types and computational values, making them expressive enough to encompass large ares of mathematics and programming. However, as the body of formal knowledge in the type theory expands, the problem of managing mathematical domains and their proofs becomes increasingly significant. Though the objects of the theory are formal, the domains are not. In this paper, we show how to apply the methods of formal data abstraction to the organization of the mathematical domains. In the process we expand the tools of data abstraction to include reusability and namespace organization, providing an environment that can be used for defining objects within a domain, for organizing domains within a type theory, and for organizing theories within a system. This environment will require extending the expressivness of inductive definitions within the type theory to include the dependent characteristics of type theoretical domains.

Note: This also contains a summary of the NuPRL type theory as an Appendix.