The PROSPER project aims at
componentizing theorem proving tools so that they can be more
widely used.
Hol98 is a Moscow ML-based
implementation of the HOL logic, incorporating many features not
found in other HOL systems. Hol98 technology
appears in tools currently under development in the PROSPER project.
This refers to an environment (currently used by
both HOL and
Isabelle/HOL) for defining and reasoning about recursive,
but total, functions in higher order logic. TFL
supports the definition of recursive functions via ML-style pattern
matching, as well as inductive proofs of properties of such
functions. I'm interested in developing a deduction-based
strong functional programming environment with it.
This was an exercise in combining two large theorem proving
systems. It was conducted in cooperation with Richard
Boulton then at Edinburgh University, now at Glasgow.