{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:12:53Z","timestamp":1767928373029,"version":"3.49.0"},"reference-count":29,"publisher":"EDP Sciences","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["RAIRO-Theor. Inf. Appl."],"published-print":{"date-parts":[[2012,7]]},"DOI":"10.1051\/ita\/2012012","type":"journal-article","created":{"date-parts":[[2012,6,22]],"date-time":"2012-06-22T19:55:45Z","timestamp":1340394945000},"page":"413-450","source":"Crossref","is-referenced-by-count":50,"title":["Probabilistic operational semantics for the lambda calculus"],"prefix":"10.1051","volume":"46","author":[{"given":"Ugo Dal","family":"Lago","sequence":"first","affiliation":[]},{"given":"Margherita","family":"Zorzi","sequence":"additional","affiliation":[]}],"member":"250","published-online":{"date-parts":[[2012,6,22]]},"reference":[{"key":"R1","doi-asserted-by":"crossref","unstructured":"P. Audebaud and C. Paulin-Mohring, Proofs of randomized algorithms in Coq, inProc. of Mathematics of Program Construction.Lect. Notes Comput. Sci.401449\u201368 (2006).","DOI":"10.1007\/11783596_6"},{"key":"R2","doi-asserted-by":"crossref","unstructured":"P.-L. Curien and H. Herbelin, The duality of computation, inProc. of International Conference on Functional Programming(2000) 233\u2013243.","DOI":"10.1145\/357766.351262"},{"key":"R3","unstructured":"U. Dal Lago and M. Zorzi, Probabilistic operational semantics for the lambda calculus. Long Version. Available at http:\/\/arxiv.org\/abs\/1104.0195, 2012."},{"key":"R4","doi-asserted-by":"crossref","unstructured":"Danvy O. and Filinski A., Representing control : A study of the CPS transformation.Math. Struct. Comput. Sci.2(1992) 361\u2013391.","DOI":"10.1017\/S0960129500001535"},{"key":"R5","unstructured":"Danvy O. and Nielsen L.R., CPS transformation of beta-redexes.Inform. Process. Lett.94(2005) 217\u2013224."},{"key":"R6","doi-asserted-by":"crossref","unstructured":"B.A. Davey and H.A. Priestley,Introduction to Lattices and Order. Cambridge University Press (2002).","DOI":"10.1017\/CBO9780511809088"},{"key":"R7","unstructured":"de\u2019 Liguoro U. and Piperno A., Nondeterministic extensions of untyped\u03bb-calculus.Inform. Comput.122(1995) 149\u2013177."},{"key":"R8","doi-asserted-by":"crossref","unstructured":"Di Pierro A., Hankin C. and Wiklicky H., Probabilistic\u03bb-calculus and quantitative program analysis.J. Logic Comput.15(2005) 159\u2013179.","DOI":"10.1093\/logcom\/exi008"},{"key":"R9","doi-asserted-by":"crossref","unstructured":"Edalat A., Domains for computation in mathematics, physics and exact real arithmetic.Bull. Symbolic Logic3(1997) 401\u2013452.","DOI":"10.2307\/421098"},{"key":"R10","doi-asserted-by":"crossref","unstructured":"A. Edalat and M.H. Escard, Integration in real PCF, inProc. of IEEE Symposium on Logic in Computer Science. Society Press (1996) 382\u2013393.","DOI":"10.1109\/LICS.1996.561453"},{"key":"R11","unstructured":"M. Gaboardi,Inductive and coinductive techniques in the operational analysis of functional programs : an introduction. Master\u2019s thesis, Universita\u2019 di Milano, Bicocca (2004)."},{"key":"R12","doi-asserted-by":"crossref","unstructured":"M. Giry, A categorical approach to probability theory, inCategorical Aspects of Topology and Analysis, edited by B. Banaschewski. Springer, Berlin, Heidelberg (1982) 68\u201385.","DOI":"10.1007\/BFb0092872"},{"key":"R13","unstructured":"Jacobs B. and Rutten J., A tutorial on (co)algebras and (co)induction.Bull. EATCS62(1996) 222\u2013259."},{"key":"R14","unstructured":"C. Jones,Probabilistic non-determinism. Ph.D. thesis, University of Edinburgh, Edinburgh, Scotland, UK (1989)."},{"key":"R15","doi-asserted-by":"crossref","unstructured":"C. Jones and G. Plotkin, A probabilistic powerdomain of evaluations, inProc. of IEEE Symposium on Logic in Computer Science. IEEE Press (1989) 186\u2013195.","DOI":"10.1109\/LICS.1989.39173"},{"key":"R16","unstructured":"Leroy X. and Grall H., Coinductive big-step operational semantics.Inform. Comput.207(2009) 284\u2013304."},{"key":"R17","doi-asserted-by":"crossref","unstructured":"E. Moggi, Computational lambda-calculus and monads, inProc. of IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press (1989) 14\u201323.","DOI":"10.1109\/LICS.1989.39155"},{"key":"R18","doi-asserted-by":"crossref","unstructured":"Moggi E., Notions of computation and monads.Inform. Comput.93(1989) 55\u201392.","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"R19","doi-asserted-by":"crossref","unstructured":"S. Park, A calculus for probabilistic languages, inProc. of ACM SIGPLAN International Workshop on Types in Languages Design and Implementation. ACM Press (2003) 38\u201349.","DOI":"10.1145\/640136.604180"},{"key":"R20","unstructured":"S. Park, F. Pfenning and S. Thrun, A monadic probabilistic language. Manuscript. Available at http:\/\/www.cs.cmu.edu\/\u02dcfp\/papers\/prob03.pdf (2003)."},{"key":"R21","doi-asserted-by":"crossref","unstructured":"S. Park, F. Pfenning and S. Thrun, A probabilistic language based upon sampling functions, inProc. of ACM Symposium on Principles of Programming Languages40(2005) 171\u2013182.","DOI":"10.1145\/1047659.1040320"},{"key":"R22","unstructured":"Plotkin G.D., Call-by-name, call-by-value and the\u03bb-calculus.Theoret. Comput. Sci.1(1975) 125\u2013159."},{"key":"R23","unstructured":"Plotkin G.D., LCF considered as a programming language.Theoret. Comput. Sci.5(1977) 223\u2013255."},{"key":"R24","doi-asserted-by":"crossref","unstructured":"N. Ramsey and A. Pfeffer, Stochastic lambda calculus and monads of probability distributions, inProc. of ACM Symposium on Principles of Programming Languages. ACM Press (2002) 154\u2013165.","DOI":"10.1145\/565816.503288"},{"key":"R25","doi-asserted-by":"crossref","unstructured":"Rutten J., Elements of Stream Calculus (An Extensive Exercise In Coinduction).Electron. Notes Theor. Comput. Sci45(2001) 358\u2013423.","DOI":"10.1016\/S1571-0661(04)80972-1"},{"key":"R26","unstructured":"Saheb-Djaromi N., Probabilistic LCF, inProc. of International Symposium on Mathematical Foundations of Computer Science.Lect. Notes Comput. Sci.64(1978) 442\u2013451."},{"key":"R27","doi-asserted-by":"crossref","unstructured":"D. Sangiorgi,Introduction to Bisimulation and Coinduction. Cambridge University Press (2012).","DOI":"10.1017\/CBO9780511777110"},{"key":"R28","unstructured":"Selinger P. and Valiron B., A lambda calculus for quantum computation with classical control.Math. Struct. Comput. Sci.16(2006) 527\u2013552."},{"key":"R29","unstructured":"C. Wadsworth, Some unusual\u03bb-calculus numeral systems, inTo H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism, edited by J.P. Seldin and J.R. Hindley. Academic Press (1980)."}],"container-title":["RAIRO - Theoretical Informatics and Applications"],"original-title":[],"link":[{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita\/2012012\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T11:52:19Z","timestamp":1743594739000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita\/2012012"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,22]]},"references-count":29,"journal-issue":{"issue":"3"},"alternative-id":["ita110023"],"URL":"https:\/\/doi.org\/10.1051\/ita\/2012012","relation":{},"ISSN":["0988-3754","1290-385X"],"issn-type":[{"value":"0988-3754","type":"print"},{"value":"1290-385X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,22]]}}}