Formal Theory in my Thesis

This page presents the formal theory given in my thesis. This presentation is only scarcely documented; for explanation I refer to my thesis. The theory is given in the format of Yarrow script files, i.e. files which can serve as input to Yarrow. In fact, the Yarrow distribution comes with all these script files.

Syntax of Yarrow script files

A Yarrow script file consists of a sequence of commands. The main commands are:

Var x:T
Adds variable x of type T to the context. These variable declarations are printed in red.
Def x:=t:T
Adds the definition of x as t of type T to the context (the :T part is optional). These definitions are printed in blue.
Prove x:T
Enters interactive proof mode to find an inhabitant of T which will be given name x. This command is printed in blue. After such a command, Yarrow files contain several commands to construct this inhabitant. These commands are printed in black.
Load
This instructs Yarrow to load another file first.
Infix, Implicit and Binder
These are instructions on how to print and parse certain constructions.
--
This signals the rest of the line is comment.

Syntax of Terms

The Yarrow syntax of terms is as follows:

\x:T.e
for a lambda abstraction
@x:T.e
for a pi-type
let x:=e:T.f
for a local definition
f e
for application (left-associative)
(e)
to deviate from standard-precedence

Precedence goes from lowest to highest, so \x:T.x x means \x:T.(x x) and not (\x:T.x) x. The lambda, pi and let terms do extend to right as far as possible.

We use the following shorthands:

\x1,x2,..xn:T.e
for a repeated abstraction
@x1,x2,..xn:T.e
for a repeated pi-type
T->U
as a short-hand for @x:T.U if x does not occur in U (the -> is right-assoc iative)

The Theory

Now for the theory itself. It is structured here according to my thesis. For a better overview, many script files come also in a version without the commands that form the proofs.

Chapter 4: lambda-omega-L, a Programming Logic

More theory in lambda-omega-L (not in thesis)

Chapter 6: lambda-omega-L-plus and Modelling Abstract Datatypes

Chapter 8: System lambda-omega-L-plus-sub, Subtyping Added

Chapter 9: Encoding Objects