Abstract
This paper is both a position paper on a particular approach in program correctness, and also a contribution to this area. The approach entails the generation of programs (code) from the executable content of logical theories. This capability already exists within the main theorem provers like Coq, Isabelle and ACL2 and PVS. Here we will focus on issues portraying the use of this methodology, rather than the underlying theory. We illustrate the power of the approach within PVS via two case studies (on unification and compression) that lead to actual running code. We also demonstrate its flexibility by extending the program generation capabilities. This paper fits in a line of ongoing integration of programming and proving.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Baader F, Snyder W (2001) Unification theory. In: Robinson A, Voronkov A, (eds) Handbook of automated reasoning, vol I, chap 8. Elsevier, Amsterdam, pp 445–532
Berghofer S, Nipkow N (2000) Executing higher order logic. In: Callaghan P, Luo Z, McKinna J, (eds) Types for Proofs and Programs, number 2277 in Lect Notes Comp Sci. Springer, Berlin Heidelberg New York, pp 24–40
Bertot Y, Castéran P (2004) Interactive theorem proving and program development Texts in Theor Comp Sci. Springer, Berlin Heidelberg New York
Burdy L, Cheon Y, Cok D, Ernst M, Kiniry J, Leavens G, Leino K, Poll E (2005) An overview of JML tools and applications. Int J Softw Tools Technol Transf 7(3):212–232
Copeland T (2005) PMD applied. Centennial Books, San Francisco
Cruz-Filipe L, Spitters B (2003) Program extraction from large proof developments. In: Basin D, Wolf B, (eds), Theorem proving in higher order logics, number 2758 in Lect Notes Comp Sci. Springer, Berlin Newyork, pp. 205–220
Hovemeyer D, Pugh W (2004) Finding bugs is easy. SIGPLAN Not., 39(12):92–106
Jacobs B, Poll E (2004) Java program verification at Nijmegen: developments and perspective. In: Futatsugi K, Mizoguchi F, Yonezaki N, (eds), Software Security—Theories and Systems, number 3233 in Lect Notes Comp Sci. Springer, Berlin, pp 134–153
Jones SLP, Wadler P (1993) Imperative functional programming. In: Conference record of the Twentieth Annual ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, pp 71–84
Kaufmann M, Manolios P, Moore J (2000) Computer-aided reasoning: An Approach. Kluwer, Newyork
Leroy X (2006) Formal certification of a compiler back-end or: programming a compiler with a proof assistant. SIGPLAN Not 41(1):42–54
Munoz C (2003) Rapid prototyping in PVS. Technical Report NIA Rep. No. 2003-03, NASA National Institute of Aerospace. http://research.nianet.org/~munoz/PVSio/
Naraschewski W, Nipkow T (1999) Type inference verified: algorithm W in Isabelle/HOL. J Automated Reasoning, 23(3–4):299–318
Necula GC (1997) Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on principles of programming languages (POPL ’97), Paris, pp 106–119
Owre S, Shankar N, Rushby J, Stringer-Calvert D (2001a) PVS language reference (version 2.4). Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA
Owre S, Shankar N, Rushby J, Stringer-Calvert D (2001b) PVS prover guide (version 2.4). Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA
Paulin-Mohring C (1989) Extracting F ω’s programs from proofs in the Calculus of Constructions. In: Principles of programming Languages, ACM Press, pp 89–104 seattle
Paulin-Mohring C, Werner B (1993) Synthesis of ML programs in the system Coq. J Sym Comput 5–6:607–640
Plasmeijer R, van Eekelen M (2001) Concurrent CLEAN Language Report (version 2.0). http://www.cs.ru.nl/~clean/.
Robinson J (1965) A machine-oriented logic based on the resolution principle. J. ACM, 12:23–41
Sanders P, Runciman C (1992) LZW text compression in Haskell. In: Launchbury J, Sansom P, (eds), Proceedings Glasgow Workshop on Functional Programming, Workshops in Computing, Ayr, Scotland. Springer, Berlin Heidelberg Newyork, pp 215–226
Welch TA (1984) A technique for high-performance data compression. IEEE Comput 17(6):8–19
Ziv J, Lempel A (1977) A universal algorithm for sequential data compression. IEEE Trans Inform Theory 23(3):337–343
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Jacobs, B., Smetsers, S. & Schreur, R.W. Code-carrying theories. Form Asp Comp 19, 191–203 (2007). https://doi.org/10.1007/s00165-006-0013-4
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-006-0013-4