{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:56:01Z","timestamp":1776891361270,"version":"3.51.2"},"reference-count":36,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"5-6","license":[{"start":{"date-parts":[[2008,8,15]],"date-time":"2008-08-15T00:00:00Z","timestamp":1218758400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2008,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checked proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. The tool's soundness theorem is expressed in terms of the bit-level semantics of x86 programs, so its correctness depends on very few assumptions. We take advantage of Coq's support for programming with dependent types and modules in the structure of the development. The approach is based on developing a library of reusable functors for transforming a verifier at one level of abstraction into a verifier at a lower level. Using this library, it is possible to prototype a verifier based on a new type system with a minimal amount of work, while obtaining a very strong soundness theorem about the final product.<\/jats:p>","DOI":"10.1017\/s0956796808006904","type":"journal-article","created":{"date-parts":[[2008,8,15]],"date-time":"2008-08-15T06:31:08Z","timestamp":1218781868000},"page":"599-647","source":"Crossref","is-referenced-by-count":4,"title":["Modular development of certified program verifiers with a proof assistant,"],"prefix":"10.46298","volume":"18","author":[{"given":"ADAM","family":"CHLIPALA","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,8,15]]},"reference":[{"key":"S0956796808006904_ref27","unstructured":"Morrisett Greg , Crary Karl , Glew Neal , Grossman Dan , Samuels Richard , Smith Frederick , Walker David , Weirich Stephanie & Zdancewic Steve . (1999b) TALx86: A realistic typed assembly language. In Proceedings of the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software. Atlanta, GA, USA, pp. 25\u201335."},{"key":"S0956796808006904_ref15","doi-asserted-by":"crossref","unstructured":"Feng Xinyu , Ni Zhaozhong , Shao Zhong & Guo Yu . (January 2007) An open framework for foundational proof-carrying code. In TLDI'07: Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation. Nice, France, pp. 67\u201378.","DOI":"10.1145\/1190315.1190325"},{"key":"S0956796808006904_ref7","unstructured":"Chang Bor-Yuh Evan , Chlipala Adam & Necula George C. (2006) A framework for certified program analysis and its applications to mobile-code safety. In VMCAI '06: Proceedings of the Seventh International Conference on Verification, Model Checking, and Abstract Interpretation. Charleston, South Carolina, USA, pp. 174\u2013189."},{"key":"S0956796808006904_ref12","unstructured":"Delahaye David . (2000) A tactic language for the system Coq. In LPAR '00: Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning. Reunion Island, France, pp. 85\u201395."},{"key":"S0956796808006904_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"S0956796808006904_ref14","volume-title":"A Discipline of Programming","author":"Dijkstra","year":"1976"},{"key":"S0956796808006904_ref22","doi-asserted-by":"crossref","unstructured":"Leroy Xavier . (2006a) Coinductive big-step operational semantics. In ESOP '06: Proceedings of the 15th European Symposium on Programming. Vienna, Austria, pp. 54\u201368.","DOI":"10.1007\/11693024_5"},{"key":"S0956796808006904_ref32","unstructured":"Sheard Tim . (2004) Languages of the future. In OOPSLA '04: Companion to the 19th Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications. Vancouver, BC, Canada, pp. 116\u2013119."},{"key":"S0956796808006904_ref9","unstructured":"Chlipala Adam . (2006) Modular development of certified program verifiers with a proof assistant. In ICFP '06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming. Portland, OR, USA, pp. 160\u2013171."},{"key":"S0956796808006904_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"S0956796808006904_ref8","doi-asserted-by":"crossref","unstructured":"Chen Chiyan & Xi Hongwei . (2005) Combining programming with theorem proving. In ICFP '05: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming. Tallinn, Estonia, pp. 66\u201377.","DOI":"10.1145\/1086365.1086375"},{"key":"S0956796808006904_ref5","doi-asserted-by":"crossref","unstructured":"Chang Bor-Yuh Evan , Chlipala Adam , Necula George C. & Schneck Robert R. (January 2005) The {open} {verifier framework for foundational verifiers. In TLDI'05: Proceedings of the 2nd ACM Workshop on Types in Language Design and Implementation, Long Beach, CA, USA.","DOI":"10.1145\/1040294.1040295"},{"key":"S0956796808006904_ref17","unstructured":"Gim\u00e9nez Eduardo . (1995) Codifying guarded definitions with recursive schemes. In TYPES '94: Selected Papers from the International Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden, pp. 39\u201359."},{"key":"S0956796808006904_ref3","volume-title":"Coq'Art: The Calculus of Inductive Constructions","author":"Bertot","year":"2004"},{"key":"S0956796808006904_ref19","unstructured":"Intel. (2006) IA-32 Intel Architecture Software Developer's Manual, Vol. 2: Instruction set reference."},{"key":"S0956796808006904_ref25","first-page":"11","article-title":"On the meanings of the logical constants and the justifications of the logical laws","volume":"1","author":"Martin-L\u00f6f","year":"1996","journal-title":"Nordic J. Philos. Logic"},{"key":"S0956796808006904_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.004"},{"key":"S0956796808006904_ref2","unstructured":"Bertot Yves . (2001) Formalizing a JVML verifier for initialization in a theorem prover. In CAV '01: Proceedings of the 13th International Conference on Computer Aided Verification. Paris, France, pp. 14\u201324."},{"key":"S0956796808006904_ref20","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.597"},{"key":"S0956796808006904_ref35","unstructured":"Westbrook Edwin , Stump Aaron & Wehrman Ian . (2005) A language-based approach to functionally correct imperative programming. In ICFP '05: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming. Tallinn, Estonia, pp. 268\u2013279."},{"key":"S0956796808006904_ref23","doi-asserted-by":"crossref","unstructured":"Leroy Xavier . (2006b) Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. In POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Charleston, SC, USA, pp. 42\u201354.","DOI":"10.1145\/1111037.1111042"},{"key":"S0956796808006904_ref33","unstructured":"Smith Frederick , Walker David & Morrisett J. Gregory . (2000) Alias types. In ESOP '00: Proceedings of the 9th European Symposium on Programming. Berlin, Germany, pp. 366\u2013381."},{"key":"S0956796808006904_ref10","unstructured":"Cousot Patrick & Cousot Radhia . (1977) Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL'77: Proceedings of the 4th ACM Symposium on Principles of Programming Languages. Los Angeles, CA, USA, pp. 234\u2013252."},{"key":"S0956796808006904_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.012"},{"key":"S0956796808006904_ref18","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000021012.97318.e9"},{"key":"S0956796808006904_ref36","doi-asserted-by":"crossref","unstructured":"Wu Dinghao , Appel Andrew W. & Stump Aaron . (2003) Foundational proof checkers with small witnesses. In PPDP '03: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. Uppsala, Sweden, pp. 264\u2013274.","DOI":"10.1145\/888251.888276"},{"key":"S0956796808006904_ref16","unstructured":"Filliatre Jean-Christophe & Letouzey Pierre . (2004) Functors for proofs and programs. In ESOP '04: Proceedings of the 13th European Symposium on Programming. Barcelona, Spain, pp. 370\u2013384."},{"key":"S0956796808006904_ref28","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004446"},{"key":"S0956796808006904_ref11","unstructured":"Crary Karl . (2003) Toward a foundational typed assembly language. In POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New Orleans, LA, USA, pp. 198\u2013212."},{"key":"S0956796808006904_ref13","unstructured":"Detlefs David L. , Leino K. Rustan M. , Nelson Greg & Saxe James B. (1998) Extended static checking. In SRC Research Report 159. Compaq Systems Research Center, Palo Alto."},{"key":"S0956796808006904_ref31","doi-asserted-by":"crossref","unstructured":"Necula George C. & Lee Peter . (1998) The design and implementation of a certifying compiler. In PLDI '98: Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation. Montreal, Quebec, Canada, pp. 333\u2013344.","DOI":"10.1145\/277650.277752"},{"key":"S0956796808006904_ref34","unstructured":"Wadler Philip . (1992) The essence of functional programming. In POPL '92: Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Albuquerque, NM, USA, pp. 1\u201314."},{"key":"S0956796808006904_ref21","unstructured":"Lerner Sorin , Millstein Todd , Rice Erika & Chambers Craig . (2005) Automated soundness proofs for dataflow analyses and transformations via local rules. In POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Long Beach, CA, USA, pp. 364\u2013377."},{"key":"S0956796808006904_ref30","doi-asserted-by":"crossref","unstructured":"Necula George C. (1997) Proof-carrying code. In POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Paris, France, pp. 106\u2013119.","DOI":"10.1145\/263699.263712"},{"key":"S0956796808006904_ref1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932501"},{"key":"S0956796808006904_ref24","doi-asserted-by":"crossref","unstructured":"MacQueen David . (1984) Modules for standard ML. In LFP '84: Proceedings of the 1984 ACM Symposium on LISP and Functional Programming. Austin, TX, USA, pp. 198\u2013207.","DOI":"10.1145\/800055.802036"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796808006904","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:11Z","timestamp":1776889151000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796808006904\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,8,15]]},"references-count":36,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2008,9]]}},"alternative-id":["S0956796808006904"],"URL":"https:\/\/doi.org\/10.1017\/s0956796808006904","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,8,15]]}}}