The Pure Type Systems (PTSs) form a family of typed lambda-calculi. On one
hand, a PTS can be seen as a concise but powerful functional programming
language. On the other hand, a PTS can be seen as a logical system. The thesis
of Erik Poll [Pol94] combines both interpretations, leading to a programming
logic called lambda-omega-L. This is a formal system for the design of and
reasoning about programs, i.e. proving programs correct with respect to a
specification.

This thesis continues the work of Poll, and is divided in two parts. The first
part gives the basic formalism and its implementation in Yarrow. Yarrow is a
tool we implemented providing machine support for PTSs in general, and
lambda-omega-L in particular. The use of Yarrow has had an important influence
on the rest of this thesis. In the second part we give several extensions of
lambda-omega-L, and show how they provide support for object-oriented
programming, a programming paradigm which has become very popular in the last
decades.

Now we consider the parts in more detail.

CONTENTS OF PART I
The basic formalism is given in Chapters 2 (PTSs) and 4 (lambda-omega-L). These
two chapters are given for reference, and are largely copied from Poll's
thesis.

Chapter 3 discusses Yarrow, the tool we implemented. First we discuss why
software support is necessary for developing theory in a PTS, and why we
developed our own tool instead of using existing software. Then we consider
Yarrow from three perspectives. First, we show how Yarrow is used. Second, we
discuss the theory behind interactive proof development in Yarrow. In
particular, we describe forward reasoning, which is a natural way of proving,
not present in existing systems similar to Yarrow. Third, we give the software
architecture of Yarrow. The main points here are Yarrow's treatment of I/O in
the purely functional language Haskell, and the communication between the user
interface and the engine. This communication is interesting since both a
textual and a graphical user interface have been implemented.

New in Chapter 4 is a modest library of theory, and the development of a small
example program together with its specification and proof of correctness, all
developed in Yarrow.

CONTENTS OF PART II
The goal of the second part is to extend lambda-omega-L in order to handle
Object-Oriented Programming (OOP). This programming paradigm has become so
popular because it helps structuring and reuse of programs. Central concepts of
this paradigm are:
* Aggregation.
  This is the pairing of data and algorithms working on that data.
* Encapsulation.
  This limits the access to data and encourages modular programming.
  Encapsulation is also known as data hiding or data abstraction.
* Inheritance.
  By inheritance, algorithms can work on related data structures, so reuse of
  programs is facilitated.
In order to cater for these concepts, we need to make several extensions to
lambda-omega-L. For aggregation we need records, for encapsulation we need
existential types, and for inheritance we need subtyping. The elaborations of
these extensions form the body of Part II.

Chapter 5 briefly introduces OOP by explaining a small example program, and
gives the central concepts of OOP with the necessary extensions of
lambda-omega-L in more detail.

Chapter 6 defines lambda-omega-L+ as the extension of lambda-omega-L with
records and existential types. The focus in this chapter lies on deriving proof
rules for these notions, i.e. logical rules for proving correctness of programs
that use records and existential types. This is quite an enterprise. First we
consider the theory of parametricity, which extends the notion of equality
between values of existential types. But parametricity is not enough. We need
additional axioms, stating the existence of so-called quotient and subset
types. Only then practical proof rules can be derived for abstract datatypes,
which form the simplest application of existential types. The use of Yarrow was
crucial for developing the complicated theory, and made the need for the
additional axioms apparent.

In Chapter 7 we consider subtyping. Instead of extending only the particular
PTS lambda-omega-L with subtyping, we have chosen to extend the whole framework
of PTSs, leading to a framework of Pure Type Systems with Subtyping. The
problem here is to show that we preserve the nice syntactical properties of
PTSs. We solve the problem by adopting a novel and rigorous design decision,
namely by defining the subtyping relation independent of typing.

In Chapter 8 we define lambda-omega-L+<, i.e. lambda-omega-L+ extended with
subtyping. We show some subtleties concerning the logical aspects of subtyping,
and give a small example program.

Chapter 9 shows how the ingredients of records, existential types and subtyping
can be used to model OOP. Our model, a slight variant of the well-known
existential model, is presented step-wise, so that OOP features are modelled
one at a time. We speculate on proof rules for objects, but do not formally
develop them.

CONTRIBUTIONS OF THIS THESIS
The three main contributions of this thesis are:
* Yarrow (Chapter 3), because it supports arbitrary PTSs, forward reasoning,
  and subtyping.
* Proof rules for abstract datatypes (Chapter 6). These rules are formally
  derived from the principle of abstraction, and justify and generalize both
  folklore proof rules and rules found in the field of algebraic
  specifications.
* The framework of Pure Type Systems with subtyping, including the development
  of its meta-theory (Chapter 7). The main attraction of the PTS framework is
  that many nice properties can be proved once for all its members. Similarly,
  our extension of this framework with subtyping is attractive because we prove
  nice properties for a class of systems with subtyping. This class includes
  several existing systems, and new systems, which can be useful in the field
  of programming and formal logic.



References
[Pol94] Erik Poll. A programming logic based on type theory. Ph.D. thesis,
        Eindhoven University of Technology, 1994.