{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T06:34:30Z","timestamp":1742970870450,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319221014"},{"type":"electronic","value":"9783319221021"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22102-1_13","type":"book-chapter","created":{"date-parts":[[2015,8,18]],"date-time":"2015-08-18T08:30:14Z","timestamp":1439886614000},"page":"203-220","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["A Formalized Hierarchy of Probabilistic System Types"],"prefix":"10.1007","author":[{"given":"Johannes","family":"H\u00f6lzl","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Lochbihler","sequence":"additional","affiliation":[]},{"given":"Dmitriy","family":"Traytel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,19]]},"reference":[{"issue":"8","key":"13_CR1","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568\u2013589 (2009)","journal-title":"Sci. Comput. Program."},{"issue":"1\u20132","key":"13_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.tcs.2004.07.019","volume":"327","author":"F Bartels","year":"2004","unstructured":"Bartels, F., Sokolova, A., de Vink, E.P.: A hierarchy of probabilistic system types. Theor. Comput. Sci. 327(1\u20132), 3\u201322 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR3","first-page":"193","volume-title":"POPL 2014","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Fournet, C., Gr\u00e9goire, B., Strub, P.Y., Swamy, N., Zanella B\u00e9guelin, S.: Probabilistic relational verification for cryptographic implementations. In: Jagannathan, S., Sewell, P. (eds.) POPL 2014, pp. 193\u2013205. ACM, New York (2014)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-319-08970-6_7","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93\u2013110. Springer, Heidelberg (2014)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/978-3-319-08970-6_8","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Cardinals in Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 111\u2013127. Springer, Heidelberg (2014)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-662-46669-8_15","volume-title":"Programming Languages and Systems","author":"JC Blanchette","year":"2015","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Witnessing (Co)datatypes. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 359\u2013382. Springer, Heidelberg (2015)"},{"key":"13_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45198-4","volume-title":"Semantics of Probabilistic Processes","author":"Y Deng","year":"2014","unstructured":"Deng, Y.: Semantics of Probabilistic Processes. Springer, Heidelberg (2014)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46669-8_4","volume-title":"Programming Languages and Systems","author":"M Eberl","year":"2015","unstructured":"Eberl, M., H\u00f6lzl, J., Nipkow, T.: A verified compiler for probability density functions. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 80\u2013104. Springer, Heidelberg (2015)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/978-3-319-08970-6_18","volume-title":"Interactive Theorem Proving","author":"J Gross","year":"2014","unstructured":"Gross, J., Chlipala, A., Spivak, D.I.: Experience implementing a performant category-theory library in Coq. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 275\u2013291. Springer, Heidelberg (2014)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Gunter, E.L.: Why we can\u2019t have SML-style datatype declarations in HOL. In: TPHOLs 1992. IFIP Transactions, vol. A-20, pp. 561\u2013568. North-Holland\/Elsevier (1993)","DOI":"10.1016\/B978-0-444-89880-7.50042-5"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"JV Harrison","year":"2005","unstructured":"Harrison, J.V.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 114\u2013129. Springer, Heidelberg (2005)"},{"issue":"2","key":"13_CR12","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1006\/inco.1998.2725","volume":"145","author":"C Hermida","year":"1998","unstructured":"Hermida, C., Jacobs, B.: Structural induction and coinduction in a fibrational setting. Inf. Comput. 145(2), 107\u2013152 (1998)","journal-title":"Inf. Comput."},{"key":"13_CR13","unstructured":"H\u00f6lzl, J.: Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic. Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2013)"},{"key":"13_CR14","unstructured":"H\u00f6lzl, J., Lochbihler, A., Traytel, D.: A zoo of probabilistic systems. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs (2015). http:\/\/afp.sf.net\/entries\/Probabilistic_System_Zoo.shtml"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and Transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131\u2013146. Springer, Heidelberg (2013)"},{"key":"13_CR16","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1016\/B978-044482830-9\/50029-1","volume-title":"Handbook of Process Algebras Chap. 11","author":"B Jonsson","year":"2001","unstructured":"Jonsson, B., Larsen, K.G., Yi, W.: Probabilistic extensions of process algebras. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebras Chap. 11, pp. 685\u2013710. Elsevier, Amsterdam (2001)"},{"issue":"1","key":"13_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comp. 94(1), 1\u201328 (1991)","journal-title":"Inf. Comp."},{"key":"13_CR18","unstructured":"Lochbihler, A.: Measure definition on streams, 24 February 2015. Archived at https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2015-February\/msg00112.html"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/978-3-319-08970-6_25","volume-title":"Interactive Theorem Proving","author":"D Matichuk","year":"2014","unstructured":"Matichuk, D., Wenzel, M., Murray, T.: An Isabelle proof method language. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 390\u2013405. Springer, Heidelberg (2014)"},{"key":"13_CR20","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"JJMM Rutten","year":"2000","unstructured":"Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249, 3\u201380 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR21","unstructured":"Sokolova, A.: Coalgebraic Analysis of Probabilistic Systems. Ph.D. thesis, Technische Universiteit Eindhoven (2005)"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co)datatypes for higher-order logic\u2013Category theory applied to theorem proving. In: LICS 2012, pp. 596\u2013605. IEEE (2012)","DOI":"10.1109\/LICS.2012.75"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS 1985, pp. 327\u2013338. IEEE (1985)","DOI":"10.1109\/SFCS.1985.12"},{"issue":"1\u20132","key":"13_CR24","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/S0304-3975(99)00035-3","volume":"221","author":"EP de Vink","year":"1999","unstructured":"de Vink, E.P., Rutten, J.J.: Bisimulation for probabilistic transition systems: a coalgebraic approach. Theor. Comput. Sci. 221(1\u20132), 271\u2013293 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR25","unstructured":"Weber, T.: Introducing a BNF for sets of bounded cardinality, 14 March 2015. Archived at https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2015-March\/msg00116.html"},{"key":"13_CR26","unstructured":"Zanella B\u00e9guelin, S.: Formal Certification of Game-Based Cryptographic Proofs. Ph.D. thesis, \u00c9cole Nationale Sup\u00e9rieure des Mines de Paris (2010)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22102-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,20]],"date-time":"2023-01-20T21:48:39Z","timestamp":1674251319000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22102-1_13"}},"subtitle":["Proof Pearl"],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319221014","9783319221021"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22102-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}