[Prev][Next][Index][Thread]
Thesis on type-theory for OOP
I am glad to announce the availability of my Ph.D. thesis, titled:
Object-Oriented Concepts and Proof Rules:
Formalization in Type Theory and
Implementation in Yarrow
Main contributions:
- A proof assistant called Yarrow providing support for Pure Type Systems.
- Formalization of proof rules for Abstract Data Types in type theory.
- Pure Type Systems with Subtyping.
A more extensive abstract is included below.
I have a limited number of printed copies left. If you are interested, please
send me an e-mail message (address: janz@cs.kun.nl) stating your full postal
address, and you will receive a copy as soon as possible (providing the demand
isn't too high).
The thesis is electronically available at the following URL.
http://www.cs.kun.nl/~janz/publications/index.html
Jan Zwanenburg
Abstract:
The Pure Type Systems (PTSs) form a well-known framework in the area of
type theory. Some members of this framework can be seen as bare functional
programming languages, and others as logics.
The PTS lambda-omega-L combines both interpretations, yielding a programming
logic in which programs and predicates can be defined, and programs can be
proved correct with respect to a specification.
In order to reason about Object-Oriented programs, several extensions of
lambda-omega-L are necessary. In this thesis two of those extensions are
studied, namely Abstract Data Types (ADTs) and subtyping.
The main difficulty in extending lambda-omega-L with ADTs is deriving the usual
proof rules for them. One ingredient for the rules is the existing notion of
parametricity. But this is not enough: we show quotient and subset types are
needed as well to derive proof rules for ADTs.
The derivation of these proof rules has been carried out in Yarrow, a newly
developed tool for PTSs.
We have chosen to extend not only lambda-omega-L with subtyping, but the
whole framework of PTSs, yielding the framework of Pure Type Systems with
Subtyping. We prove that extending the framework preserves many nice
properties. In this way we show that all instances of the framework behave
well. Some of these instances are interesting as a programming language, and
others as logics.