FS0 in Isabelle: adding structure at the metalevel.

San Matthews
Max-Planck-Institut fuer Informatik,
Im Stadtwald, D-66123 Saarbruecken, Germany

We describe an implementation of Feferman's theory FS0 in Isabelle. We believe this implementation makes a particularly interesting case study because, while a naive implementation of FS0 is easy to build using the standard interface that Isabelle provides, this implementation is not practially usable.

We will discuss the front end we have built on top of Isabelle, and this naive implementation. This systematically expolits the facilities of Isabelle to provide a very usable implementation, providing the tools we need for structured development of large systems in FS0, while preserving, underneath, the very simple structure of the system as Feferman describes it.

We shall also describe some of the development work we have done in our implementation (the final argument for its practicality).