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.

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.

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`

ifx does not occur in `U`

(the`->`

is right-assoc iative)

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.

- The definition of the DPTS lambda-omega-L (Section 4.3).

`lambdaL`

- The axioms and library for predicate logic
(in Section 4.4 and 4.5 respectively).

`logic`

full or without proofs. - The axioms and library for booleans
(in Section 4.4 and 4.5 respectively).

`bool`

full or without proofs. - The axioms and library for natural numbers
(in Section 4.4 and 4.5 respectively).

`nat`

full or without proofs. - The axioms and library for lists
(in Section 4.4 and 4.5 respectively).

`list`

full or without proofs. - The example of sorting
(Section 4.6).

`sort`

full or without proofs.

- More library for predicate logic.

`logic2`

full or without proofs. - More library for booleans.

`bool2`

full or without proofs. - More library for natural numbers.

`nat2`

full or without proofs. - More library for lists.

`list2`

full or without proofs.

- The definition of the DPTS lambda-omega-L-plus (Section 6.1).

`lambdaLplus`

full or without proofs. - Axioms for lambda-omega-L-plus (Section 6.2).

`LOLP_Axioms`

full or without proofs. - The example of stacks (Section 6.3).

`stack`

full or without proofs. - Some preliminary definitions (Section 6.7.1).
We need these definitions for the example of bags.

`prelims`

full or without proofs. - The example of bags: implementation 1 (Section 6.5.1).

`bag1`

full or without proofs. - The example of bags: implementation 2 (Section 6.5.2).

`bag2`

full or without proofs. - The example of bags: implementation 3 (Section 6.5.3).

`bag3`

full or without proofs. - Parametricity and first-order interfaces (Section 6.7.2 and 6.7.3).

`parametricity`

full or without proofs. - The library leading to the main theorems (Section 6.7.4 up to 6.7.6).

`library`

full or without proofs. - The main results about axiomatizing quotients and subsets (Section 6.8).

`axiomatizing`

full or without proofs.

- The definition of the DPTS lambda-omega-L-plus-sub (Section 8.1.2).

`lambdaLsubplus`

- The (very small) library (Section 8.3.1).

`subLibrary`

full or without proofs. - The example of sorting of records
(Section 8.4).

`sortId`

full or without proofs.

- Aggregation (Section 9.1).

`pointDevelop1`

- Encapsulation (Section 9.2).

`pointDevelop2`

- Subtyping (Section 9.3).

`pointDevelop3`