{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:59Z","timestamp":1780994699152,"version":"3.54.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319898834","type":"print"},{"value":"9783319898841","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89884-1_8","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T21:02:32Z","timestamp":1523653352000},"page":"214-241","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus"],"prefix":"10.1007","author":[{"given":"Alejandro","family":"Aguirre","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ale\u0161","family":"Bizjak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: The guarded lambda-calculus: programming and reasoning with guarded recursion for coinductive types. Log. Methods Comput. Sci. 12(3) (2016)","DOI":"10.2168\/LMCS-12(3:7)2016"},{"issue":"ICFP","key":"8_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3110265","volume":"1","author":"Alejandro Aguirre","year":"2017","unstructured":"Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.: A relational logic for higher-order programs. PACMPL 1(ICFP), 21:1\u201321:29 (2017)","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"8_CR3","unstructured":"Lindvall, T.: Lectures on the Coupling Method. Courier Corporation (2002)"},{"key":"8_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1236-2","volume-title":"Coupling, Stationarity, and Regeneration","author":"H Thorisson","year":"2000","unstructured":"Thorisson, H.: Coupling, Stationarity, and Regeneration. Springer, New York (2000)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-662-48899-7_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Barthe","year":"2015","unstructured":"Barthe, G., Espitau, T., Gr\u00e9goire, B., Hsu, J., Stefanesco, L., Strub, P.-Y.: Relational reasoning via probabilistic coupling. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 387\u2013401. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_27"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Hsu, J., Strub, P.: Coupling proofs are probabilistic product programs. In: POPL 2017, Paris, France, 18\u201320 January 2017 (2017)","DOI":"10.1145\/3009837.3009896"},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1214\/aoms\/1177700153","volume":"36","author":"V Strassen","year":"1965","unstructured":"Strassen, V.: The existence of probability measures with given marginals. Ann. Math. Stat. 36, 423\u2013439 (1965)","journal-title":"Ann. Math. Stat."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"issue":"6","key":"8_CR9","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/s10207-012-0177-2","volume":"11","author":"D Bogdanov","year":"2012","unstructured":"Bogdanov, D., Niitsoo, M., Toft, T., Willemson, J.: High-performance secure multi-party computation for data mining applications. Int. J. Inf. Sec. 11(6), 403\u2013418 (2012)","journal-title":"Int. J. Inf. Sec."},{"key":"8_CR10","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107337756","volume-title":"Secure Multiparty Computation and Secret Sharing","author":"R Cramer","year":"2015","unstructured":"Cramer, R., Damgard, I.B., Nielsen, J.B.: Secure Multiparty Computation and Secret Sharing, 1st edn. Cambridge University Press, New York (2015)","edition":"1"},{"key":"8_CR11","unstructured":"Barthe, G., Espitau, T., Gr\u00e9goire, B., Hsu, J., Strub, P.: Proving uniformity and independence by self-composition and coupling. CoRR abs\/1701.06477 (2017)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: Proceedings of Foundations of Computer Science. IEEE (2001)","DOI":"10.1109\/SFCS.2001.959888"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-662-49630-5_2","volume-title":"Foundations of Software Science and Computation Structures","author":"A Bizjak","year":"2016","unstructured":"Bizjak, A., Grathwohl, H.B., Clouston, R., M\u00f8gelberg, R.E., Birkedal, L.: Guarded dependent type theory with coinductive types. In: Jacobs, B., L\u00f6ding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 20\u201335. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_2"},{"issue":"1","key":"8_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796807006326","volume":"18","author":"C McBride","year":"2008","unstructured":"McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1\u201313 (2008)","journal-title":"J. Funct. Program."},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, R.E., Schwinghammer, J., St\u00f8vring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Log. Methods Comput. Sci. 8(4) (2012)","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0037118","volume-title":"Typed Lambda Calculi and Applications","author":"G Plotkin","year":"1993","unstructured":"Plotkin, G., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 361\u2013375. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0037118"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Dreyer, D., Ahmed, A., Birkedal, L.: Logical step-indexed logical relations. Log. Methods Comput. Sci. 7(2) (2011)","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In: Morrisett, G., Uustalu, T. (eds.) ICFP 2013, Boston, MA, USA, 25\u201327 September 2013. ACM (2013)","DOI":"10.1145\/2500365.2500600"},{"issue":"1","key":"8_CR19","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1145\/3093333.3009855","volume":"52","author":"Robbert Krebbers","year":"2017","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: Castagna, G., Gordon, A.D. (eds.) POPL 2017, Paris, France, 18\u201320 January 2017. ACM (2017)","journal-title":"ACM SIGPLAN Notices"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Krogh-Jespersen, M., Svendsen, K., Birkedal, L.: A relational model of types-and-effects in higher-order concurrent separation logic. In: POPL 2017, Paris, France, 18\u201320 January 2017, pp. 218\u2013231 (2017)","DOI":"10.1145\/3009837.3009877"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45842-5_1","volume-title":"Types for Proofs and Programs","author":"P Aczel","year":"2002","unstructured":"Aczel, P., Gambino, N.: Collection principles in dependent type theory. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 1\u201323. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45842-5_1"},{"issue":"1","key":"8_CR22","doi-asserted-by":"publisher","first-page":"67","DOI":"10.2178\/jsl\/1140641163","volume":"71","author":"P Aczel","year":"2006","unstructured":"Aczel, P., Gambino, N.: The generalised type-theoretic interpretation of constructive set theory. J. Symb. Log. 71(1), 67\u2013103 (2006)","journal-title":"J. Symb. Log."},{"key":"8_CR23","unstructured":"Grimm, N., Maillard, K., Fournet, C., Hritcu, C., Maffei, M., Protzenko, J., Rastogi, A., Swamy, N., B\u00e9guelin, S.Z.: A monadic framework for relational verification (functional pearl). CoRR abs\/1703.00055 (2017)"},{"key":"8_CR24","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 $$\\lambda $$\u03bb-calculi. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 209\u2013228. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_12"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D., Vignudelli, V.: Environmental bisimulations for probabilistic higher-order languages. In: Bod\u00edk, R., Majumdar, R. (eds.) POPL 2016, St. Petersburg, FL, USA, 20\u201322 January 2016. ACM (2016)","DOI":"10.1145\/2837614.2837651"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-662-46678-0_18","volume-title":"Foundations of Software Science and Computation Structures","author":"A Bizjak","year":"2015","unstructured":"Bizjak, A., Birkedal, L.: Step-indexed logical relations for probability. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 279\u2013294. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46678-0_18"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Borgstr\u00f6m, J., Lago, U.D., Gordon, A.D., Szymczak, M.: A lambda-calculus foundation for universal probabilistic programming. In: Garrigue, J., Keller, G., Sumii, E. (eds.) ICFP 2016, Nara, Japan, 18\u201322 September 2016. ACM (2016)","DOI":"10.1145\/2951913.2951942"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-662-54434-1_14","volume-title":"Programming Languages and Systems","author":"R Culpepper","year":"2017","unstructured":"Culpepper, R., Cobb, A.: Contextual equivalence for probabilistic programs with continuous random variables and scoring. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 368\u2013392. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_14"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Jones, C., Plotkin, G.D.: A probabilistic powerdomain of evaluations. In: LICS 1989, Pacific Grove, California, USA, 5\u20138 June 1989. IEEE Computer Society (1989)","DOI":"10.1109\/LICS.1989.39173"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Staton, S., Yang, H., Wood, F., Heunen, C., Kammar, O.: Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In: LICS 2016, New York, NY, USA, 5\u20138 July 2016. ACM (2016)","DOI":"10.1145\/2933575.2935313"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Barthe, G., Fournet, C., Gr\u00e9goire, B., Strub, P., Swamy, N., B\u00e9guelin, S.Z.: Probabilistic relational verification for cryptographic implementations. In: Jagannathan, S., Sewell, P. (eds.) POPL 2014 (2014)","DOI":"10.1145\/2535838.2535847"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gaboardi, M., Gallego Arias, E.J., Hsu, J., Roth, A., Strub, P.Y.: Higher-order approximate relational refinement types for mechanism design and differential privacy. In: POPL 2015, Mumbai, India, 15\u201317 January 2015 (2015)","DOI":"10.1145\/2676726.2677000"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Barthe, G., Farina, G.P., Gaboardi, M., Arias, E.J.G., Gordon, A., Hsu, J., Strub, P.: Differentially private Bayesian programming. In: CCS 2016, Vienna, Austria, 24\u201328 October 2016. ACM (2016)","DOI":"10.1145\/2976749.2978371"},{"issue":"3\u20134","key":"8_CR34","first-page":"211","volume":"9","author":"C Dwork","year":"2014","unstructured":"Dwork, C., Roth, A.: The algorithmic foundations of differential privacy. Found. Trends Theor. Comput. Sci. 9(3\u20134), 211\u2013407 (2014)","journal-title":"Found. Trends Theor. Comput. Sci."},{"issue":"12","key":"8_CR35","first-page":"1155","volume":"7","author":"G Kellaris","year":"2014","unstructured":"Kellaris, G., Papadopoulos, S., Xiao, X., Papadias, D.: Differentially private event sequences over infinite streams. PVLDB 7(12), 1155\u20131166 (2014)","journal-title":"PVLDB"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89884-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:32:39Z","timestamp":1571157159000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89884-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319898834","9783319898841"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}