KnowledgeBase » SEMINAR » ID = 416

The Ultimate Programming Machine II: Very Dependent Types

by Jason Hickey
1994-1995

This seminar will be a continuation of the PRL seminar I gave on October 25. During the last seminar I presented additions to the Nuprl type theory that I would eventually use to build a high level language with formal abstract data types and inheritance (which provides the foundation for a formal object-oriented language). The types that I presented provide the ability to express very dependent functions.

During the next seminar, I will discuss further enhancements to the Nuprl programming language, including some practical derived types and pattern matching. I will then develop a few more derived types that are steps on the way to full abstract data type. These types are derived in the sense that they can be formulated in the existing type theory. The derived types include the very-dependent W type to describe very dependent trees, a recursive module mechanism to describe very dependent DAGs, and finally the theory type, which is a type I use to describe all formal abstract data types with inheritence.