{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:10:53Z","timestamp":1750306253182,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":14,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,16]],"date-time":"2017-01-16T00:00:00Z","timestamp":1484524800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["Ni 491\/16-1"],"award-info":[{"award-number":["Ni 491\/16-1"]}],"id":[{"id":"10.13039\/501100001659","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.3018628","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T21:20:29Z","timestamp":1482441629000},"page":"100-111","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Markov processes in Isabelle\/HOL"],"prefix":"10.1145","author":[{"given":"Johannes","family":"H\u00f6lzl","sequence":"first","affiliation":[{"name":"TU M\u00fcnchen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,1,16]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.002"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1212357"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_4"},{"key":"e_1_3_2_1_6_1","series-title":"Lecture Notes in Mathematics","first-page":"85","volume-title":"Categorical Aspects of Topology and Analysis","author":"Giry M.","year":"1982","unstructured":"M. Giry . A categorical approach to probability theory . In Categorical Aspects of Topology and Analysis , volume 915 of Lecture Notes in Mathematics , pages 68\u2013 85 , 1982 . M. Giry. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis, volume 915 of Lecture Notes in Mathematics, pages 68\u201385, 1982."},{"key":"e_1_3_2_1_7_1","volume-title":"The Archive of Formal Proofs","author":"Gouezel S.","year":"2015","unstructured":"S. Gouezel . Ergodic theory . The Archive of Formal Proofs , Dec 2015 . ISSN 2150-914x. https:\/\/www.isa-afp.org\/ entries\/Ergodic_Theory.shtml, (Formal proof development). T. C. Hales, M. Adams, G. Bauer, D. T. Dang, J. Harrison, T. L. Hoang, C. Kaliszyk, V. Magron, S. McLaughlin, T. T. Nguyen, T. Q. Nguyen, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, A. H. T. Ta, T. N. Tran, D. T. Trieu, J. Urban, K. K. Vu, and R. Zumkeller. A formal proof of the kepler conjecture. CoRR, abs\/1501.02155, 2015. S. Gouezel. Ergodic theory. The Archive of Formal Proofs, Dec 2015. ISSN 2150-914x. https:\/\/www.isa-afp.org\/ entries\/Ergodic_Theory.shtml, (Formal proof development). T. C. Hales, M. Adams, G. Bauer, D. T. Dang, J. Harrison, T. L. Hoang, C. Kaliszyk, V. Magron, S. McLaughlin, T. T. Nguyen, T. Q. Nguyen, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, A. H. T. Ta, T. N. Tran, D. T. Trieu, J. Urban, K. K. Vu, and R. Zumkeller. A formal proof of the kepler conjecture. CoRR, abs\/1501.02155, 2015."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"J.\n      H\u00f6lzl\n    .\n  Markov chains and Markov decision processes in Isabelle\/HOL 2016\n  . Submitted to JAR in December 2015 (http:\/\/in.tum.de\/~hoelzl\/mdptheory). J. H\u00f6lzl and A. Heller. Three chapters of measure theory in Isabelle\/HOL. In M. C. J. D. van Eekelen H. Geuvers J. Schmaltz and F. Wiedijk editors Interactive Theorem Proving (ITP\n   2011) volume \n  6898\n   of \n  LNCS pages 135\u2013\n  151\n  . Springer 2011.   J. H\u00f6lzl. Markov chains and Markov decision processes in Isabelle\/HOL 2016. Submitted to JAR in December 2015 (http:\/\/in.tum.de\/~hoelzl\/mdptheory). J. H\u00f6lzl and A. Heller. Three chapters of measure theory in Isabelle\/HOL. In M. C. J. D. van Eekelen H. Geuvers J. Schmaltz and F. Wiedijk editors Interactive Theorem Proving (ITP 2011) volume 6898 of LNCS pages 135\u2013151. Springer 2011.","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.08.005"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1345169.1345171"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_22"},{"key":"e_1_3_2_1_14_1","volume-title":"Cambridge Series in Statistical and Probabilisitc Mathematics","author":"Norris J. R.","year":"1997","unstructured":"J. R. Norris . Markov Chains . Cambridge Series in Statistical and Probabilisitc Mathematics . Cambridge University Press , 1997 . J. R. Norris. Markov Chains. Cambridge Series in Statistical and Probabilisitc Mathematics. Cambridge University Press, 1997."},{"key":"e_1_3_2_1_15_1","series-title":"Cambridge Series in Statistical and Probabilistic Mathematics","volume-title":"A Users\u2019s Guide to Measure Theoretic Probability","author":"Pollard D.","year":"2002","unstructured":"D. Pollard . A Users\u2019s Guide to Measure Theoretic Probability . Cambridge Series in Statistical and Probabilistic Mathematics . Cambridge University Press , 2002 . D. Pollard. A Users\u2019s Guide to Measure Theoretic Probability. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, 2002."},{"key":"e_1_3_2_1_16_1","volume-title":"Probability and Statistics with Reliability, Queuing and Computer Science Applications","author":"Trivedi K. S.","year":"2002","unstructured":"K. S. Trivedi . Probability and Statistics with Reliability, Queuing and Computer Science Applications . Wiley , 2 nd edition edition, 2002 . K. S. Trivedi. Probability and Statistics with Reliability, Queuing and Computer Science Applications. Wiley, 2nd edition edition, 2002.","edition":"2"},{"key":"e_1_3_2_1_17_1","unstructured":"Introduction Related Work Preliminaries Discrete-Time Markov Processes Continuous-Time Markov Chains Conclusion and Discussion  Introduction Related Work Preliminaries Discrete-Time Markov Processes Continuous-Time Markov Chains Conclusion and Discussion"}],"event":{"name":"CPP '17: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Paris France","acronym":"CPP '17"},"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.3018628","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3018610.3018628","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:59Z","timestamp":1750220639000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018628"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,16]]},"references-count":14,"alternative-id":["10.1145\/3018610.3018628","10.1145\/3018610"],"URL":"https:\/\/doi.org\/10.1145\/3018610.3018628","relation":{},"subject":[],"published":{"date-parts":[[2017,1,16]]},"assertion":[{"value":"2017-01-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}