kirancodes.me
To Proof Maintenance & Beyond!
ASE 2005

Prufrock: a framework for constructing polytypic theorem provers

Justin Ward, Garrin Kimmell, Perry Alexander

PDFDOI 10.1145/1101908.1101985dblp

Abstract

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 reasoning systems, which abstracts semantic concerns over entire classes of potential implementation languages. Prufrock utilizes polytypic programming techniques to create independent, reusable modules defining proof in different logics, independent of the language used to represent formulae in the logic, as well as the exact implementation of low-level prover functionality.

BibTeX
@inproceedings{Ward-al:ASE05,
  author    = {Justin Ward and
               Garrin Kimmell and
               Perry Alexander},
  title     = {Prufrock: a framework for constructing polytypic theorem provers},
  booktitle = {ASE},
  pages     = {423--426},
  publisher = {{ACM}},
  year      = {2005},
}

Related papers