## Deliverables: a categorical approach to program development in
type theory

**James Hugh McKinna**
*Abstract:* This thesis considers the problem of program
correctness within a rich theory of dependent types, the Extended
Calculus of Constructions (ECC). This system contains a powerful
programming language of higher-order primitive recursion and
higher-order intuitionistic logic. It is supported by Pollack's
versatile LEGO implementation, which I use extensively to develop
the mathematical constructions studied here.

I systematically investigate Burstall's notion of
*deliverable*, that is, a program paired with a proof of
correctness. This approach separates the concerns of programming
and logic, since I want a simple program extraction mechanism. The
Sigma-types of the calculus enable us to achieve this. There are
many similarities with the subset interpretation of Martin-Löf
type theory.

I show that deliverables have a rich categorical structure, so
that correctness proofs may be decomposed in a principled way. The
categorical combinators which I define in the system package up
much logical book-keeping, allowing one to concentrate on the
essential structure of algorithms.

I demonstrate our methodology with a number of small examples,
culminating in a machine-checked proof of the Chinese remainder
theorem, showing the utility of the deliverables idea. Some
drawbacks are also encountered.

I consider also semantic aspects of deliverables, examining the
definitions in an abstract setting, again firmly based on category
theory. The aim is to overcome the clumsiness of the language of
categorical combinators, using dependent type theories and their
interpretation in fibrations. I elaborate a concrete instance based
on the category of sets, which generalises to an arbitrary topos.
In the process, I uncover a subsystem of ECC within which one may
speak of deliverables defined over the topos. In the presence of
enough extra structure, the interpretation extends to the whole of
ECC. The wheel turns full circle.

**PhD Thesis - Price £9.00**

*LFCS report ECS-LFCS-92-247 (also published as
CST-96-92)*

This thesis is available as five separate files: 1, 2,
3, 4, 5.

Previous |

Index |

Next