{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:18:07Z","timestamp":1763468287149,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,18]],"date-time":"2017-01-18T00:00:00Z","timestamp":1484697600000},"content-version":"vor","delay-in-days":366,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000140","name":"U.S. Department of Transportation","doi-asserted-by":"publisher","award":["DTRT12GUTC11"],"award-info":[{"award-number":["DTRT12GUTC11"]}],"id":[{"id":"10.13039\/100000140","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Future Of Life Institute","award":["FLI-RFP-AI1"],"award-info":[{"award-number":["FLI-RFP-AI1"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1054246"],"award-info":[{"award-number":["CNS-1054246"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,18]]},"DOI":"10.1145\/2854065.2854078","type":"proceedings-article","created":{"date-parts":[[2016,1,12]],"date-time":"2016-01-12T08:18:57Z","timestamp":1452586737000},"page":"110-121","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics"],"prefix":"10.1145","author":[{"given":"Nathan","family":"Fulton","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,1,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33353-8_2"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646874.709849"},{"key":"e_1_3_2_1_3_1","series-title":"Handbook of Philosophical Logic","first-page":"360","volume-title":"Handbook of Philosophical Logic","author":"Artemov S.","unstructured":"S. Artemov and L. Beklemishev. Provability Logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, 2nd Edition, volume 13 of Handbook of Philosophical Logic, pages 189\u2013 360. Springer Netherlands, 2005.","edition":"2"},{"key":"e_1_3_2_1_4_1","unstructured":"S. N. Artemov. Operational modal logic. Technical Report MSI 9529 Cornell University 1995."},{"key":"e_1_3_2_1_5_1","volume-title":"Berlin, Germany","author":"de Moura L. M.","year":"2015","unstructured":"L. M. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 378\u2013388, 2015."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.04.009"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"N. Fulton S. Mitsch J.-D. Quesel M. V\u00f6lp and A. Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In A. P. Felty and A. Middeldorp editors CADE volume 9195 of LNCS pages 527\u2013538. Springer 2015.","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"e_1_3_2_1_8_1","unstructured":"N. Fulton and A. Platzer. A logic of proofs for differential dynamic logic: Tech report. Technical Report CMU-CS-15-143 School of Computer Science Carnegie Mellon University Pittsburgh PA 2015."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/646184.682934"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_2"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190245"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","unstructured":"S. M. Loos A. Platzer and L. Nistor. Adaptive cruise control: Hybrid distributed and now formally verified. In M. Butler and W. Schulte editors FM volume 6664 of LNCS pages 42\u201356. Springer 2011.","DOI":"10.5555\/2021296.2021304"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461350"},{"key":"e_1_3_2_1_15_1","series-title":"Dagstuhl Seminar Proceedings","volume-title":"Mathematics, Algorithms, Proofs","author":"Mahboubi A.","year":"2005","unstructured":"A. Mahboubi. Programming and certifying the cad algorithm inside the coq system. In Mathematics, Algorithms, Proofs, volume 05021 of Dagstuhl Seminar Proceedings, Schloss Dagstuhl, 2005."},{"volume-title":"The Coq proof assistant reference manual","year":"2004","key":"e_1_3_2_1_16_1","unstructured":"The Coq development team. The Coq proof assistant reference manual, 2004. Version 8.0."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1791547"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753634"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","unstructured":"A. Platzer. Differential dynamic logic for verifying parametric hybrid systems. In N. Olivetti editor TABLEAUX volume 4548 of LNCS pages 216\u2013232. Springer 2007. 10.1007\/978-3-540-73099-6_17","DOI":"10.1007\/978-3-540-73099-6_17"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1869900"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.13"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2817824"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"A. Platzer. A uniform substitution calculus for differential dynamic logic. In A. P. Felty and A. Middeldorp editors CADE volume 9195 of LNCS pages 467\u2013481. Springer 2015.","DOI":"10.1007\/978-3-319-21401-6_32"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","unstructured":"A. Platzer and E. M. Clarke. Formal verification of curved flight collision avoidance maneuvers: A case study. In A. Cavalcanti and D. Dams editors FM volume 5850 of LNCS pages 547\u2013562. Springer 2009. 10.1007\/978-3-642-05089-3_35","DOI":"10.1007\/978-3-642-05089-3_35"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","unstructured":"A. Platzer and J.-D. Quesel. KeYmaera: A hybrid theorem prover for hybrid systems. In A. Armando P. Baumgartner and G. Dowek editors IJCAR volume 5195 of LNCS pages 171\u2013178. Springer 2008. 10.1007\/978-3-540-71070-7_15","DOI":"10.1007\/978-3-540-71070-7_15"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","unstructured":"A. Platzer and J.-D. Quesel. European Train Control System: A case study in formal verification. In K. Breitman and A. Cavalcanti editors ICFEM volume 5885 of LNCS pages 246\u2013265. Springer 2009. 10.1007\/978-3-642-10373-5_13","DOI":"10.1007\/978-3-642-10373-5_13"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","unstructured":"A. Platzer J.-D. Quesel and P. R\u00fcmmer. Real world verification. In R. A. Schmidt editor CADE volume 5663 of LNCS pages 485\u2013501. Springer 2009. 10.1007\/978-3-642-02959-2_35","DOI":"10.1007\/978-3-642-02959-2_35"},{"key":"e_1_3_2_1_30_1","volume-title":"How to model and prove hybrid systems with KeYmaera: A tutorial on safety","author":"Quesel J.-D.","year":"2015","unstructured":"J.-D. Quesel, S. Mitsch, S. Loos, N. Ar\u00e9chiga, and A. Platzer. How to model and prove hybrid systems with KeYmaera: A tutorial on safety. 2015."},{"key":"e_1_3_2_1_31_1","series-title":"Lecture Notes in Computer Science","first-page":"386","volume-title":"Logical Foundations of Computer Science","author":"Woltzenlogel Paleo B.","unstructured":"B. Woltzenlogel Paleo. Contextual natural deduction. In S. Artemov and A. Nerode, editors, Logical Foundations of Computer Science, volume 7734 of Lecture Notes in Computer Science, pages 372\u2013386. Springer Berlin Heidelberg, 2013."}],"event":{"name":"CPP 2016: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"St. Petersburg FL USA","acronym":"CPP 2016"},"container-title":["Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854078","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2854065.2854078","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2854065.2854078","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:52:10Z","timestamp":1763459530000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854078"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,18]]},"references-count":31,"alternative-id":["10.1145\/2854065.2854078","10.1145\/2854065"],"URL":"https:\/\/doi.org\/10.1145\/2854065.2854078","relation":{},"subject":[],"published":{"date-parts":[[2016,1,18]]},"assertion":[{"value":"2016-01-18","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}