{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:03:21Z","timestamp":1770289401336,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540440390","type":"print"},{"value":"9783540456858","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_16","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T16:47:53Z","timestamp":1179593273000},"page":"230-245","source":"Crossref","is-referenced-by-count":17,"title":["A Formal Approach to Probabilistic Termination"],"prefix":"10.1007","author":[{"given":"Joe","family":"Hurd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"16_CR1","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"16_CR2","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, 1993."},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Sergiu Hart, Micha Sharir, and Amir Pnueli. Termination of probabilistic concurrent programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 5(3):356\u2013380, July 1983.","DOI":"10.1145\/2166.357214"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Jifeng He, K. Seidel, and A. McIver. Probabilistic models for the guarded command language. Science of Computer Programming, 28(2\u20133):171\u2013192, April 1997.","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"16_CR5","unstructured":"Joe Hurd. Verification of the Miller-Rabin probabilistic primality test. In Richard J. Boulton and Paul B. Jackson, editors, TPHOLs 2001: Supplemental Proceedings, number EDI-INF-RR-0046 in University of Edinburgh Informatics Report Series, pages 223\u2013238, September 2001."},{"key":"16_CR6","unstructured":"Joe Hurd. Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge, 2002."},{"key":"16_CR7","unstructured":"Claire Jones. Probabilistic Non-Determinism. PhD thesis, University of Edinburgh, 1990."},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Dexter Kozen. Semantics of probabilistic programs. In 20th Annual Symposium on Foundations of Computer Science, pages 101\u2013114, Long Beach, Ca., USA, October 1979. IEEE Computer Society Press.","DOI":"10.1109\/SFCS.1979.38"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"John Launchbury and Simon L. Peyton Jones. Lazy functional state threads. In SIGPLAN Symposium on Programming Language Design and Implementation (PLDI\u201994), Orlando, pages 24\u201335, June 1994.","DOI":"10.1145\/773473.178246"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Carroll Morgan. Proof rules for probabilistic loops. In Proceedings of the BCSFACS 7th Refinement Workshop, 1996.","DOI":"10.14236\/ewic\/RW1996.10"},{"key":"16_CR11","unstructured":"Carroll Morgan, Annabelle McIver, Karen Seidel, and J. W. Sanders. Probabilistic predicate transformers. Technical Report TR-4-95, Oxford University Computing Laboratory Programming Research Group, February 1995."},{"key":"16_CR12","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511814075","volume-title":"Randomized Algorithms","author":"R. Motwani","year":"1995","unstructured":"Rajeev Motwani and Prabhakar Raghavan. Randomized Algorithms. Cambridge University Press, Cambridge, England, June 1995."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Philip Wadler. The essence of functional programming. In 19th Symposium on Principles of Programming Languages. ACM Press, January 1992.","DOI":"10.1145\/143165.143169"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T01:38:23Z","timestamp":1587519503000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}