Prufrock: a framework for constructing polytypic theorem provers

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.

REFERENCES

• 1: P. Alexander, D. Barton, and C. Kong. Rosetta Usage Guide. The University of Kansas Information and Telecommunications Technology Center, 2335 Irving Hill Rd, Lawrence, KS.
• 2: P. Alexander, D. Barton, C. Kong, and C. Menon. The rosetta strawman. Technical report, The University of Kansas, 2002.
• 3: R. Hinze and J. Jeuring. Generic haskell: practice and theory, 2003.
• 4: Patrik Jansson , Johan Jeuring, PolyP—a polytypic programming language extension, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.470-482, January 15-17, 1997, Paris, France [doi>10.1145/263699.263763]
• 5: Patrik Jansson , Johan Jeuring, Polytypic unification, Journal of Functional Programming, v.8 n.5, p.527-536, September 1998 [doi>10.1017/S095679689800313X]
• 6: P. Jansson and J. Jeuring. A framework for polytypic programming on terms, with an application to rewriting. In WGP. Utrecht University, 2000. UU-CS-2000-19.
• 7: Johan Jeuring , Patrik Jansson, Polytypic Programming, Advanced Functional Programming, Second International School-Tutorial Text, p.68-114, August 26-30, 1996
• 8: S. P. Jones, M. P. Jones, and E. Meijer. Type classes: Exploring the design space. In Proceedings of the Haskell Workshop, Amsterdam, June 1997.
• 9: E. Komp, G. Kimmell, J. Ward, and P. Alexander. The Raskell Evaluation Environment. Technical report, The University of Kansas Information and Telecommunications Technology Center, 2335 Irving Hill Rd, Lawrence, KS, USA, November 2003.
• 10: R. Kumar, T. Kropf, and K. Schneider. Integrating a First-Order Automatic Prover in the HOL Environment. In M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 170--176, Davis, California, 1991. IEEE Computer Society Press.
• 11: U. Norell and P. Jansson. Polytypic programming in haskell, 2004.
• 12: Lawrence C. Paulson, ML for the working programmer (2nd ed.), Cambridge University Press, New York, NY, 1996
• 13: Geoff Sutcliffe , Christian Suttner, The TPTP Problem Library, Journal of Automated Reasoning, v.21 n.2, p.177-203, October 1998 [doi>10.1023/A:1005806324129]
• 14: J. Ward and G. Kimmell. Rosetta Theorem Prover. Technical Report, The University of Kansas Information and Telecommunications Technology Center, 2335 Irving Hill Rd, Lawrence, KS, USA, June 2003.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

General Terms:
Design

Keywords:
Haskell, polytypic programming, type classes