{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:46:10Z","timestamp":1768002370431,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,16]],"date-time":"2018-01-16T00:00:00Z","timestamp":1516060800000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-2-0291"],"award-info":[{"award-number":["FA8750-12-2-0291"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"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"}]},{"DOI":"10.13039\/501100001866","name":"Fonds National de la Recherche Luxembourg","doi-asserted-by":"publisher","award":["FNR\/P14\/8149128"],"award-info":[{"award-number":["FNR\/P14\/8149128"]}],"id":[{"id":"10.13039\/501100001866","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1,16]]},"DOI":"10.1145\/3018610.3018616","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"208-221","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":43,"title":["Formally verified differential dynamic logic"],"prefix":"10.1145","author":[{"given":"Rose","family":"Bohrer","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Vincent","family":"Rahli","sequence":"additional","affiliation":[{"name":"University of Luxembourg, Luxembourg"}]},{"given":"Ivana","family":"Vukotic","sequence":"additional","affiliation":[{"name":"University of Luxembourg, Luxembourg"}]},{"given":"Marcus","family":"V\u00f6lp","sequence":"additional","affiliation":[{"name":"University of Luxembourg, Luxembourg"}]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,1,16]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Coq Proof Assistant."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2001.930163"},{"key":"e_1_3_2_1_3_1","unstructured":"930163."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.005"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"A. Anand and R. A. Knepper. ROSCoq: Robots powered by constructive reals. In C. Urban and X. Zhang editors ITP 2015 volume 9236 of LNCS pages 34\u201350. Springer 2015. ISBN 978-3-319-22101-4.","DOI":"10.1007\/978-3-319-22102-1_3"},{"key":"e_1_3_2_1_6_1","first-page":"44","volume-title":"Klein and Gamboa {25}","author":"Anand A.","unstructured":"A. Anand and V. Rahli. Towards a formally verified proof assistant. In Klein and Gamboa {25}, pages 27\u201344. ISBN 978- 3-319-08969-0."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065"},{"key":"e_1_3_2_1_8_1","first-page":"4503","volume":"978","author":"ACM","unstructured":"ACM. ISBN 978-1-4503-4127-1.","journal-title":"ISBN"},{"key":"e_1_3_2_1_9_1","volume-title":"INRIA Rocquencourt","author":"Barras B.","year":"1997","unstructured":"B. Barras and B. Werner. Coq in Coq. Technical report, INRIA Rocquencourt, 1997."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","unstructured":"D. A. Basin and D. J. Howe. Some normalization properties of Martin-L\u00f6f\u2019s type theory and applications. In T. Ito and A. R. Meyer editors TACS \u201991 volume 526 of LNCS pages 475\u2013494. Springer 1991. ISBN 3-540-54415-1.","DOI":"10.5555\/645867.670922"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_3_2_1_12_1","series-title":"LNCS","volume-title":"ITP\u201913","author":"Blazy S.","year":"2013","unstructured":"S. Blazy, C. Paulin-Mohring, and D. Pichardie, editors. ITP\u201913, volume 7998 of LNCS, 2013. Springer. ISBN 978- 3-642-39633-5."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0181-1"},{"key":"e_1_3_2_1_14_1","volume-title":"Introduction to Mathematical Logic","author":"Church A.","year":"1956","unstructured":"A. Church. Introduction to Mathematical Logic. Princeton, Princeton University Press, 1956."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/10510"},{"key":"e_1_3_2_1_16_1","series-title":"LNCS","volume-title":"CADE-25","author":"Felty A. P.","year":"2015","unstructured":"A. P. Felty and A. Middeldorp, editors. CADE-25, volume 9195 of LNCS, 2015. Springer. ISBN 978-3-319-21400-9."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","unstructured":"G. Frehse C. L. Guernic A. Donz\u00e9 S. Cotton R. Ray O. Lebeltel R. Ripado A. Girard T. Dang and O. Maler. SpaceEx: Scalable verification of hybrid systems. In G. Gopalakrishnan and S. Qadeer editors CAV 2011 volume 6806 of LNCS pages 379\u2013395. Springer 2011. ISBN 978- 3-642-22109-5.","DOI":"10.5555\/2032305.2032335"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854078"},{"key":"e_1_3_2_1_19_1","unstructured":"2854078."},{"key":"e_1_3_2_1_20_1","unstructured":"2854078."},{"key":"e_1_3_2_1_21_1","first-page":"538","volume-title":"Felty and Middeldorp {14}","author":"Fulton N.","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 Felty and Middeldorp {14}, pages 527\u2013538. ISBN 978-3-319-21400-9."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","unstructured":"J. Harrison. Towards self-verification of HOL Light. In U. Furbach and N. Shankar editors IJCAR 2006 volume 4130 of LNCS pages 177\u2013191. Springer 2006. ISBN 3-540- 37187-7. 10.1007\/11814771_17","DOI":"10.1007\/11814771_17"},{"key":"e_1_3_2_1_23_1","unstructured":"J. H\u00f6lzl F. Immler and B. Huffman. Type classes and filters for mathematical analysis in Isabelle\/HOL. In Blazy et al."},{"key":"e_1_3_2_1_24_1","first-page":"642","volume":"978","unstructured":", pages 279\u2013294. ISBN 978-3-642-39633-5.","journal-title":"ISBN"},{"key":"e_1_3_2_1_25_1","volume-title":"2nd Coq Workshop","author":"Hur C.-K.","year":"2010","unstructured":"C.-K. Hur. Heq: a Coq library for heterogeneous equality. Presented at the 2nd Coq Workshop, 2010."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","unstructured":"F. Immler. Verified reachability analysis of continuous systems. In C. Baier and C. Tinelli editors TACAS-21 volume 9035 of LNCS pages 37\u201351. Springer 2015. ISBN 978- 3-662-46680-3. 10.1007\/978-3-662-46681-0_3","DOI":"10.1007\/978-3-662-46681-0_3"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"F. Immler and C. Traut. The flow of ODEs. In J. C. Blanchette and S. Merz editors ITP 2016 volume 9807 of LNCS pages 184\u2013199. Springer 2016. ISBN 978-3-319-43143-7.","DOI":"10.1007\/978-3-319-43144-4_12"},{"key":"e_1_3_2_1_28_1","volume-title":"STTT","author":"Jeannin J.","year":"2016","unstructured":"J. Jeannin, K. Ghorbal, Y. Kouskoulas, A. Schmidt, R. Gardner, S. Mitsch, and A. Platzer. A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. STTT, 2016."},{"issue":"1","key":"e_1_3_2_1_29_1","first-page":"27","article-title":"Computing with classical real numbers","volume":"2","author":"Kaliszyk C.","year":"2009","unstructured":"C. Kaliszyk and R. O\u2019Connor. Computing with classical real numbers. J. Formalized Reasoning, 2(1):27\u201339, 2009.","journal-title":"J. Formalized Reasoning"},{"key":"e_1_3_2_1_30_1","series-title":"LNCS","volume-title":"ITP","author":"Klein G.","year":"2014","unstructured":"G. Klein and R. Gamboa, editors. ITP 2014, volume 8558 of LNCS, 2014. Springer. ISBN 978-3-319-08969-0."},{"key":"e_1_3_2_1_31_1","volume-title":"Type classes for efficient exact real arithmetic in Coq. Logical Methods in Computer Science, 9(1)","author":"Krebbers R.","year":"2011","unstructured":"R. Krebbers and B. Spitters. Type classes for efficient exact real arithmetic in Coq. Logical Methods in Computer Science, 9(1), 2011."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9357-x"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/646874.709976"},{"key":"e_1_3_2_1_35_1","unstructured":"ISBN 3-540-57318-6."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2670529.2754966"},{"key":"e_1_3_2_1_37_1","first-page":"436","volume-title":"Klein and Gamboa {25}","author":"Myreen M. O.","unstructured":"M. O. Myreen and J. Davis. The reflective Milawa theorem prover is sound - (down to the machine code that runs it). In Klein and Gamboa {25}, pages 421\u2013436. ISBN 978-3-319-08969-0."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_38"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/1791547"},{"key":"e_1_3_2_1_40_1","series-title":"LNCS","volume-title":"Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow)","author":"Paulson L. C.","year":"1994","unstructured":"L. C. Paulson. Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow), volume 828 of LNCS. Springer, 1994. ISBN 3-540-58244-4."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","unstructured":"A. M. Pitts. Nominal logic: A first order theory of names and binding. In N. Kobayashi and B. C. Pierce editors TACS 2001 volume 2215 of LNCS pages 219\u2013242. Springer 2001.","DOI":"10.5555\/645870.668672"},{"key":"e_1_3_2_1_42_1","unstructured":"ISBN 3-540-42736-8."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.13"},{"key":"e_1_3_2_1_45_1","first-page":"481","volume-title":"Felty and Middeldorp {14}","author":"Platzer A.","unstructured":"A. Platzer. A uniform substitution calculus for differential dynamic logic. In Felty and Middeldorp {14}, pages 467\u2013481. ISBN 978-3-319-21400-9."},{"key":"e_1_3_2_1_46_1","volume-title":"Autom. Reas.","author":"Platzer A.","year":"2016","unstructured":"A. Platzer. A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reas., 2016."},{"key":"e_1_3_2_1_47_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. ISBN 978-3-642-02958-5. 10.1007\/978-3-642-02959-2_35","DOI":"10.1007\/978-3-642-02959-2_35"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0367-0"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854077"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2015.7340492"},{"key":"e_1_3_2_1_51_1","volume-title":"ADPM2000","author":"V\u00f6lker N.","year":"2000","unstructured":"N. V\u00f6lker. Towards a HOL framework for the deductive analysis of hybrid control systems. In ADPM2000, 2000."}],"event":{"name":"CPP '17: Certified Proofs and Programs","location":"Paris France","acronym":"CPP '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018616","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3018610.3018616","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3018610.3018616","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:35:15Z","timestamp":1763458515000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018616"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,16]]},"references-count":51,"alternative-id":["10.1145\/3018610.3018616","10.1145\/3018610"],"URL":"https:\/\/doi.org\/10.1145\/3018610.3018616","relation":{},"subject":[],"published":{"date-parts":[[2017,1,16]]},"assertion":[{"value":"2017-01-16","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}