Prufrock: a framework for constructing polytypic theorem provers

Current formal software engineering methodologies provide a vast array of languages for specifying correctness properties, as well as a wide assortment automated tools that aid in the verification of specified properties. Unfortunately, the implementation of each such tool requires an early commitment to a particular methodology and language, in terms of both high-level semantic concerns and the lower-level syntactic representations of properties and proofs. In this paper, we present Prufrock, a novel approach to automated g systems, which abstracts semantic concerns over entire classes of potential implementation languages. Prufrock is a modular prover framework written in the Haskell programming language. It consists of a set of largely independent logic modules, which define the semantics required for proof over entire classes of abstract syntaxes, using polytypic programming techniques. Any given representation language may be used for specifying and verifying properties in Pru...

• Type: Conference
• Year: 2005
• Where: KBSE
• Authors: Justin Ward, Garrin Kimmell, Perry Alexander
• Keywords: Correctness Properties, Implementation, KBSE 2005, Semantic Concerns, Software Engineering