Code-carrying theories

B.P.F. Jacobs, S. Smetsers, R. Wichers Schreur

    Research output: Contribution to journalArticleAcademicpeer-review

    6 Citations (Scopus)


    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.
    Original languageEnglish
    Pages (from-to)191-203
    JournalFormal Aspects of Computing
    Issue number2
    Publication statusPublished - 2007


    Dive into the research topics of 'Code-carrying theories'. Together they form a unique fingerprint.

    Cite this