PRL Seminars

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.