ACS Project Proposals by Prof L C Paulson
Formalising the Top 100 Theorems using Isabelle
There was an online list (archived here) of 100 well-known mathematical theorems, and a separate list indicating how many of these have been formalised in a variety of different interactive theorem provers. As of this writing, 49 of them had been formalised in Isabelle, the top system being HOL Light at 85.
The project is merely to identify and prove (using Isabelle) a selection of the not-yet-formalised theorems. The selection needs to be done with care, since typically a theorem is proved in the context of possibly a very substantial theory, which would also have to be developed by proof rather than assumed as a collection of axioms. It is also possible to include theorems that have been proved already, using a different proof. (Some theorems have several substantially different proofs.) It is acceptable to follow an existing HOL Light formalisation, but more interesting is to formalise a textbook development.
It is equally acceptable to formalise interesting theorems not on that list, such as Goodstein's theorem.
This project will suit students who have a mathematical background, especially if they are already familiar with the theorems that they choose to formalise.
A Formal Model of IEEE Floating Point in Isabelle, with Applications
To verify programs that use floating point computation, it is necessary to have a formal model of the IEEE floating point standard. Such a model exists for the interactive theorem prover HOL4. Translating this model to Isabelle should be relatively straightforward, since the logical formalisms are very similar. This would open the prospect of being able to verify and execute the same formal specification, thanks to Isabelle's code generation mechanism. Any number of case studies, large or small, could be built upon this basis.
A Formalisation of Information Theory
Shannon's information theory is fundamental to many aspects of computer science, including cryptography, coding theory, data transmission and compression. It rests on an elaborate mathematical basis that includes integration theory, measure theory and probability theory. Most of this foundation has already been laid: a simple formalisation of information theory already exists in Isabelle. However, many of the fundamental theorems of information theory have yet to be formalised. A paper describing similar work conducted using the Coq system illustrates some of the tasks to be undertaken. Note that Coq proofs cannot easily be ported to Isabelle, because the logical formalisms are very different.