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

• 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 theory in lambda-omega-L (not in thesis)

• 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.

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

• 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.

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

• 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.

Chapter 9: Encoding Objects

• Aggregation (Section 9.1).
  pointDevelop1
• Encapsulation (Section 9.2).
  pointDevelop2
• Subtyping (Section 9.3).
  pointDevelop3