{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T18:41:39Z","timestamp":1770835299616,"version":"3.50.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2219757"],"award-info":[{"award-number":["CCF-2219757"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006168","name":"National Nuclear Security Administration","doi-asserted-by":"publisher","award":["DE-NA0003525"],"award-info":[{"award-number":["DE-NA0003525"]}],"id":[{"id":"10.13039\/100006168","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>Intermediate verification languages like Why3 and Boogie have made it much easier to build program verifiers, transforming the process into a logic compilation problem rather than a proof automation one. Why3 in particular implements a rich logic for program specification with polymorphism, algebraic data types, recursive functions and predicates, and inductive predicates; it translates this logic to over a dozen solvers and proof assistants. Accordingly, it serves as a backend for many tools, including Frama-C, EasyCrypt, and GNATProve for Ada SPARK. But how can we be sure that these tools are correct? The alternate foundational approach, taken by tools like VST and CakeML, provides strong guarantees by implementing the entire toolchain in a proof assistant, but these tools are harder to build and cannot directly take advantage of SMT solver automation. As a first step toward enabling automated tools with similar foundational guarantees, we give a formal semantics in Coq for the logic fragment of Why3. We show that our semantics are useful by giving a correct-by-construction natural deduction proof system for this logic, using this proof system to verify parts of Why3\u2019s standard library, and proving sound two of Why3\u2019s transformations used to convert terms and formulas into the simpler logics supported by the backend solvers.<\/jats:p>","DOI":"10.1145\/3632902","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1789-1818","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["A Formalization of Core Why3 in Coq"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9555-8781","authenticated-orcid":false,"given":"Joshua M.","family":"Cohen","sequence":"first","affiliation":[{"name":"Princeton University, Princeton, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5973-0671","authenticated-orcid":false,"given":"Philip","family":"Johnson-Freyd","sequence":"additional","affiliation":[{"name":"Sandia National Laboratories, Livermore, United States"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.3"},{"key":"e_1_3_1_3_1","unstructured":"AdaCore and Altran UK Ltd. 2018. SPARK 2014 User\u2019s Guide: Release 19.0w."},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_3"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/1695"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_3_1_9_1","first-page":"53","volume-title":"Boogie 2011: First International Workshop on Intermediate Verification Languages","author":"Bobot Fran\u00e7ois","year":"2011","unstructured":"Fran\u00e7ois Bobot, Jean-Christophe Filli\u00e2tre, Claude March\u00e9, and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wroclaw, Poland, 53\u201364. https:\/\/inria.hal.science\/hal-00790310"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9153.001.0001"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Joshua M. Cohen and Philip Johnson-Freyd. 2023. POPL Artifact for \"A Formalization of Core Why3 in Coq\". https:\/\/doi.org\/10.5281\/zenodo.8417774 10.5281\/zenodo.8417774","DOI":"10.5281\/zenodo.8417774"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_1"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-36755-8_4"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/jjlamp.2023.100871"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.336.2"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/1979"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_2"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/38.2.131"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(3:19)2015"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_5"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_8"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_6"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_16"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/925926"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_33"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_31"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1774088.1774610"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632911"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632902","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632902","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632902","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:02:08Z","timestamp":1751659328000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632902"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":43,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632902"],"URL":"https:\/\/doi.org\/10.1145\/3632902","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}