Formal Abstract Data Types and Inheritance

by Jason Hickey
1995-1996

Abstract

Currently, many formal systems have developed tools for writing and verifying algorithms, but little support has been given to modularity. Often, programs exist in a flat space, or in a space with partitions provided by the filesystem. In this talk, I propose a more formal approach to modularity that treats abstract data types (ADTs) as first class objects, and provides a link between ADTs and formal theories.

In addition, ADTs can be extended so that all properties of the ADT remain true of the extension. These two features--abstraction and inheritance--form the basis for formal object-oriented programming. Near the end of the talk, I will give a proposal for a Grand Unified Theory of programming, equating all of the different kinds of formal assertions.

This talk will not require any knowledge of Nuprl.

Formal Abstract Data Types and Inheritance

by Jason Hickey 1995-1996

by Jason Hickey
1995-1996