{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:05Z","timestamp":1750221305886,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,8]],"date-time":"2018-01-08T00:00:00Z","timestamp":1515369600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"French National Research Agency (ANR)","award":["ANR-11-IDEX-0007"],"award-info":[{"award-number":["ANR-11-IDEX-0007"]}]},{"name":"European Research Council (ERC)","award":["678157"],"award-info":[{"award-number":["678157"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,1,8]]},"DOI":"10.1145\/3167088","type":"proceedings-article","created":{"date-parts":[[2018,3,16]],"date-time":"2018-03-16T16:10:56Z","timestamp":1521216656000},"page":"42-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Completeness and decidability of converse PDL in the constructive type theory of Coq"],"prefix":"10.1145","author":[{"given":"Christian","family":"Doczkal","sequence":"first","affiliation":[{"name":"University of Lyon, France \/ CNRS, France \/ ENS Lyon, France \/ Claude Bernard University Lyon 1, France \/ LIP, France"}]},{"given":"Joachim","family":"Bard","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}]}],"member":"320","published-online":{"date-parts":[[2018,1,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.02.036"},{"volume-title":"Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem, and Frank Wolter (Eds.). Studies in Logic and Practical Reasoning","author":"Baader Franz","key":"e_1_3_2_2_3_1","unstructured":"Franz Baader and Carsten Lutz . 2007. Description Logic . In Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem, and Frank Wolter (Eds.). Studies in Logic and Practical Reasoning , Vol. 3 . Elsevier , 757\u2013820. Franz Baader and Carsten Lutz. 2007. Description Logic. In Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem, and Frank Wolter (Eds.). Studies in Logic and Practical Reasoning, Vol. 3. Elsevier, 757\u2013820."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01257083"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.02.004"},{"key":"e_1_3_2_2_7_1","volume-title":"Accessed Nov. 17th","author":"Cohen Cyril","year":"2017","unstructured":"Cyril Cohen . 2017 . A finset and finmap DRAFT library. https:\/\/github. com\/math-comp\/finmap . (Nov. 2017) . Accessed Nov. 17th , 2017. Cyril Cohen. 2017. A finset and finmap DRAFT library. https:\/\/github. com\/math-comp\/finmap . (Nov. 2017). Accessed Nov. 17th, 2017."},{"key":"e_1_3_2_2_9_1","unstructured":"Christian Doczkal and Joachim Bard. 2017. Coq development accompanying this paper. https:\/\/github.com\/chdoc\/comp-dec-pdl . (2017).  Christian Doczkal and Joachim Bard. 2017. Coq development accompanying this paper. https:\/\/github.com\/chdoc\/comp-dec-pdl . (2017)."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9361-9"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90001-7"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_3_2_2_13_1","unstructured":"Dov M. Gabbay. 1977. Axiomatization of Logic Programs. (1977). Text of a letter to V. Pratt.  Dov M. Gabbay. 1977. Axiomatization of Logic Programs. (1977). Text of a letter to V. Pratt."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/557365"},{"volume-title":"TABLEAUX 2011 (LNCS (LNAI)), Kai Br\u00fcnnler and George Metcalfe (Eds.)","author":"Kaminski Mark","key":"e_1_3_2_2_17_1","unstructured":"Mark Kaminski , Thomas Schneider , and Gert Smolka . 2011. Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics . In TABLEAUX 2011 (LNCS (LNAI)), Kai Br\u00fcnnler and George Metcalfe (Eds.) , Vol. 6793 . Springer , 196\u2013210. Mark Kaminski, Thomas Schneider, and Gert Smolka. 2011. Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics. In TABLEAUX 2011 (LNCS (LNAI)), Kai Br\u00fcnnler and George Metcalfe (Eds.), Vol. 6793. Springer, 196\u2013210."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90019-0"},{"volume-title":"Mathematical Foundations of Computer Science (LNCS), J\u00f3zef Winkowski (Ed.)","author":"Parikh Rohit","key":"e_1_3_2_2_19_1","unstructured":"Rohit Parikh . 1978. The Completeness of Propositional Dynamic Logic . In Mathematical Foundations of Computer Science (LNCS), J\u00f3zef Winkowski (Ed.) , Vol. 64 . Springer , 403\u2013415. Rohit Parikh. 1978. The Completeness of Propositional Dynamic Logic. In Mathematical Foundations of Computer Science (LNCS), J\u00f3zef Winkowski (Ed.), Vol. 64. Springer, 403\u2013415."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_15"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1979.24"},{"key":"e_1_3_2_2_22_1","volume-title":"A Completeness Theorem in the Modal Logic of Programs. Notices Amer. Math. Soc. 24","author":"Segerberg Krister","year":"1977","unstructured":"Krister Segerberg . 1977. A Completeness Theorem in the Modal Logic of Programs. Notices Amer. Math. Soc. 24 ( 1977 ), A\u2013 552. Krister Segerberg. 1977. A Completeness Theorem in the Modal Logic of Programs. Notices Amer. Math. Soc. 24 (1977), A\u2013552."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.49.6.828"},{"key":"e_1_3_2_2_24_1","first-page":"41","article-title":"A New Look at Generalized Rewriting in Type Theory","volume":"2","author":"Sozeau Matthieu","year":"2009","unstructured":"Matthieu Sozeau . 2009 . A New Look at Generalized Rewriting in Type Theory . J. Form. Reason. 2 , 1 (2009), 41 \u2013 62 . Matthieu Sozeau. 2009. A New Look at Generalized Rewriting in Type Theory. J. Form. Reason. 2, 1 (2009), 41\u201362.","journal-title":"J. Form. Reason."},{"key":"e_1_3_2_2_25_1","unstructured":"The Mathematical Components team. 2017. Mathematical Components. (2017). http:\/\/math-comp.github.io\/math-comp\/  The Mathematical Components team. 2017. Mathematical Components. (2017). http:\/\/math-comp.github.io\/math-comp\/"}],"event":{"name":"CPP '18: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Los Angeles CA USA","acronym":"CPP '18"},"container-title":["Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167088","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167088","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:28Z","timestamp":1750212808000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167088"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,8]]},"references-count":20,"alternative-id":["10.1145\/3167088","10.1145\/3176245"],"URL":"https:\/\/doi.org\/10.1145\/3167088","relation":{},"subject":[],"published":{"date-parts":[[2018,1,8]]},"assertion":[{"value":"2018-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}