{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:51Z","timestamp":1780994691245,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466773","type":"print"},{"value":"9783662466780","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46678-0_18","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T13:42:21Z","timestamp":1427895741000},"page":"279-294","source":"Crossref","is-referenced-by-count":27,"title":["Step-Indexed Logical Relations for Probability"],"prefix":"10.1007","author":[{"given":"Ale\u0161","family":"Bizjak","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Ahmed, A.: Semantics of Types for Mutable State. Ph.D. thesis, Princeton University (2004)"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/11693024_6","volume-title":"Programming Languages and Systems","author":"A. Ahmed","year":"2006","unstructured":"Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 69\u201383. Springer, Heidelberg (2006)"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems\u00a023(5) (2001)","DOI":"10.1145\/504709.504712"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Bizjak, A., Schwinghammer, J.: Step-indexed relational reasoning for countable nondeterminism. Logical Methods in Computer Science 9(4) (2013)","DOI":"10.2168\/LMCS-9(4:4)2013"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Reus, B., Schwinghammer, J., St\u00f8vring, K., Thamsborg, J., Yang, H.: Step-indexed kripke models over recursive worlds. In: Proceedings of the 38th Symposium on Principles of Programming Languages, pp. 119\u2013132. ACM (2011)","DOI":"10.1145\/1926385.1926401"},{"key":"18_CR6","unstructured":"Bizjak, A., Birkedal, L.: Step-indexed logical relations for probability. arXiv:1501.02623 [cs.LO] (2015), long version of this paper"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-54833-8_12","volume-title":"Programming Languages and Systems","author":"R. Crubill\u00e9","year":"2014","unstructured":"Crubill\u00e9, R., Dal Lago, U.: On probabilistic applicative bisimulation and call-by-value \u03bb-calculi. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol.\u00a08410, pp. 209\u2013228. Springer, Heidelberg (2014)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Dal Lago, U., Sangiorgi, D., Alberti, M.: On coinductive equivalences for higher-order probabilistic functional programs. In: Proceedings of 41st Symposium on Principles of Programming Languages, pp. 297\u2013308. ACM (2014)","DOI":"10.1145\/2535838.2535872"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Danos, V., Harmer, R.S.: Probabilistic game semantics. ACM Transactions on Computational Logic 3(3) (2002)","DOI":"10.1145\/507382.507385"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Dreyer, D., Ahmed, A., Birkedal, L.: Logical step-indexed logical relations. Logical Methods in Computer Science 7(2) (2011)","DOI":"10.2168\/LMCS-7(2:16)2011"},{"issue":"4-5 special iss","key":"18_CR11","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1017\/S095679681200024X","volume":"22","author":"D. Dreyer","year":"2012","unstructured":"Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming\u00a022(4-5 special issue), 477\u2013528 (2012)","journal-title":"Journal of Functional Programming"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Ehrhard, T., Pagani, M., Tasson, C.: The computational meaning of probabilistic coherence spaces. In: Proceedings of the 26th IEEE Symposium on Logic in Computer Science, pp. 87\u201396. IEEE (2011)","DOI":"10.1109\/LICS.2011.29"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Ehrhard, T., Tasson, C., Pagani, M.: Probabilistic coherence spaces are fully abstract for probabilistic pcf. In: Proceedings of 41st Symposium on Principles of Programming Languages, pp. 309\u2013320. ACM (2014)","DOI":"10.1145\/2535838.2535865"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Johann, P., Simpson, A., Voigtl\u00e4nder, J.: A generic operational metatheory for algebraic effects. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, pp. 209\u2013218. IEEE (2010)","DOI":"10.1109\/LICS.2010.29"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Jones, C., Plotkin, G.: A probabilistic powerdomain of evaluations. In: Proceedings of the 4th Symposium on Logic in Computer Science, pp. 186\u2013195. IEEE (1989)","DOI":"10.1109\/LICS.1989.39173"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Lago, U.D., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO - Theoretical Informatics and Applications 46 (2012)","DOI":"10.1051\/ita\/2012012"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Pitts, A.M.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10(3) (2000)","DOI":"10.1017\/S0960129500003066"},{"key":"18_CR18","unstructured":"Pitts, A.M.: Typed operational reasoning. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, ch. 7. MIT Press (2005)"},{"key":"18_CR19","unstructured":"Pitts, A.M.: Step-indexed biorthogonality: a tutorial example. In: Ahmed, A., Benton, N., Birkedal, L., Hofmann, M. (eds.) Modelling, Controlling and Reasoning About State. No. 10351 in Dagstuhl Seminar Proceedings (2010)"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: Proceedings of the 29th Symposium on Principles of Programming Languages, pp. 154\u2013165. ACM (2002)","DOI":"10.1145\/565816.503288"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Saheb-Djahromi, N.: Cpo\u2019s of measures for nondeterminism. Theoretical Computer Science 12(1) (1980)","DOI":"10.1016\/0304-3975(80)90003-1"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46678-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:57:42Z","timestamp":1747857462000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46678-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466773","9783662466780"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46678-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}