{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,9]],"date-time":"2023-05-09T21:10:29Z","timestamp":1683666629489},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T00:00:00Z","timestamp":1180656000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2007,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/s00165-006-0013-4","type":"journal-article","created":{"date-parts":[[2006,11,27]],"date-time":"2006-11-27T17:17:41Z","timestamp":1164647861000},"page":"191-203","source":"Crossref","is-referenced-by-count":7,"title":["Code-carrying theories"],"prefix":"10.1145","volume":"19","author":[{"given":"Bart","family":"Jacobs","sequence":"first","affiliation":[{"name":"Institute for Computing and Information Sciences, Radboud University Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sjaak","family":"Smetsers","sequence":"additional","affiliation":[{"name":"Institute for Computing and Information Sciences, Radboud University Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ronny Wichers","family":"Schreur","sequence":"additional","affiliation":[{"name":"Institute for Computing and Information Sciences, Radboud University Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1016\/B978-044450813-3\/50010-2","volume-title":"Handbook of automated reasoning, vol I, chap 8.","author":"Baader F","year":"2001"},{"key":"e_1_2_1_2_2_2","first-page":"24","volume-title":"Types for Proofs and Programs, number 2277 in Lect Notes Comp Sci.","author":"Berghofer S","year":"2000"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_1_2_5_2","volume-title":"PMD applied","author":"Copeland T","year":"2005"},{"key":"e_1_2_1_2_6_2","first-page":"205","volume-title":"Theorem proving in higher order logics, number 2758 in Lect Notes Comp Sci.","author":"Cruz-Filipe L","year":"2003"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/1052883.1052895"},{"key":"e_1_2_1_2_8_2","first-page":"134","volume-title":"Software Security\u2014Theories and Systems, number 3233 in Lect Notes Comp Sci.","author":"Jacobs B","year":"2004"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Jones SLP Wadler P (1993) Imperative functional programming. In: Conference record of the Twentieth Annual ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages Charleston South Carolina pp 71\u201384","DOI":"10.1145\/158511.158524"},{"key":"e_1_2_1_2_10_2","volume-title":"Computer-aided reasoning: An Approach","author":"Kaufmann M","year":"2000"},{"issue":"1","key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1145\/1111320.1111042","article-title":"Formal certification of a compiler back-end or: programming a compiler with a proof assistant","volume":"41","author":"Leroy X","year":"2006","journal-title":"SIGPLAN Not"},{"key":"e_1_2_1_2_12_2","unstructured":"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\/"},{"issue":"3","key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1023\/A:1006277616879","article-title":"Type inference verified: algorithm W in Isabelle\/HOL","volume":"23","author":"Naraschewski W","year":"1999","journal-title":"J Automated Reasoning"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Necula GC (1997) Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on principles of programming languages (POPL \u201997) Paris pp 106\u2013119","DOI":"10.1145\/263699.263712"},{"key":"e_1_2_1_2_15_2","unstructured":"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"},{"key":"e_1_2_1_2_16_2","unstructured":"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"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Paulin-Mohring C (1989) Extracting F \u03c9 \u2019s programs from proofs in the Calculus of Constructions. In: Principles of programming Languages ACM Press pp 89\u2013104 seattle","DOI":"10.1145\/75277.75285"},{"issue":"6","key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","article-title":"Synthesis of ML programs in the system Coq","volume":"5","author":"Paulin-Mohring C","year":"1993","journal-title":"J Sym Comput"},{"key":"e_1_2_1_2_19_2","unstructured":"Plasmeijer R van Eekelen M (2001) Concurrent CLEAN Language Report (version 2.0). http:\/\/www.cs.ru.nl\/~clean\/."},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_2_21_2","first-page":"215","volume-title":"Proceedings Glasgow Workshop on Functional Programming, Workshops in Computing, Ayr, Scotland.","author":"Sanders P","year":"1992"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1984.1659158"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1977.1055714"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-006-0013-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-006-0013-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-006-0013-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,9]],"date-time":"2023-05-09T20:53:11Z","timestamp":1683665591000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-006-0013-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2007,6]]}},"alternative-id":["10.1007\/s00165-006-0013-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-006-0013-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,6]]}}}