Prufrock is a polytypic first-order theorem proving framework written in Haskell. Our primary application for Prufrock is verification of Rosetta specifications in the Raskell evaluation environment. Prufrock is not a specific theorem prover in the traditional sense, but rather a framework in which theorem provers can be built. Prufrock is written in Haskell and is based upon the polytypic programming research being conducted at Chalmers.

Prufrock provides a definition of proof in various logical systems separate from the specific term language used to represent assumptions and obligations. Dependencies between assorted logics are coded directly, so that first order logic, for instance, is simply an extension of the rules and operations of propositional logic, adding the notion of quantifiers. This approach has many advantages, the largest of which is the separation of concerns related to proof technique and methodology from those related to a specific implementation of such techniques to a particular language.

The appropriate Haskell class instances for proving in Rosetta and the standard TPTP syntax have already been implemented.