On the face of it, these areas seem to be quite disconnected. However the notion of types provides a conceptual link. The vast majority of the formal systems that are implemented by interactive theorem provers are so-called type theories. Chapter 2 focuses on using types for proofs: after an introduction to the history of formal systems and how they gave rise to types, the objectives and principles of interactive theorem proving are highlighted. Then an application of interactive theorem proving is described: Olaf Müller and myself developed a formalization of the theory of timed I/O automata, thus providing proof support for reasoning about timed distributed systems.
In the context of programming languages, types are ubiquitous. Chapter 3 first explores the basic concept underlying all applications of type systems in programming languages: restricting the number of possible programs that can be written in order to gain additional knowledge about the legal programs. Then, type-directed partial evaluation, a particular instance of using the information provided by types, is examined. Finally a small research project (joint work with Zhe Yang) in the context of type-directed partial evaluation is described.
The fourth chapter, which in the original progress report outlines some ideas for further research, is not intended for the public and thus has been excluded.
In the report, a working knowledge of logic and functional programming is assumed.
Here are pointers to the progress report: