{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:07:09Z","timestamp":1784232429862,"version":"3.55.0"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T00:00:00Z","timestamp":1680739200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100020884","name":"Agencia Nacional de Investigaci&oacute;n y Desarrollo","doi-asserted-by":"publisher","award":["3200583"],"award-info":[{"award-number":["3200583"]}],"id":[{"id":"10.13039\/501100020884","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Hong Kong Research Grants Council","award":["17209520, 17209821"],"award-info":[{"award-number":["17209520, 17209821"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,4,6]]},"abstract":"<jats:p>Probabilistic programming languages have recently gained a lot of attention, in particular due to their applications in domains such as machine learning and differential privacy. To establish invariants of interest, many such languages include some form of static checking in the form of type systems. However, adopting such a type discipline can be cumbersome or overly conservative.  \nGradual typing addresses this problem by supporting a smooth transition between static and dynamic checking, and has been successfully applied for languages with different constructs and type abstractions. Nevertheless, its benefits have never been explored in the context of probabilistic languages.  \nIn this work, we present and formalize GPLC, a gradual source probabilistic lambda calculus. GPLC includes a binary probabilistic choice operator and allows programmers to gradually introduce\/remove static type\u2013and probability\u2013annotations. The static semantics of GPLC heavily relies on the notion of probabilistic couplings, as required for defining several relations, such as consistency, precision, and consistent transitivity. The dynamic semantics of GPLC is given via elaboration to the target language TPLC, which features a distribution-based semantics interpreting programs as probability distributions over final values. Regarding the language metatheory, we establish that TPLC\u2013and therefore also GPLC\u2013is type safe and satisfies two of the so-called refined criteria for gradual languages, namely, that it is a conservative extension of a fully static variant and that it satisfies the gradual guarantee, behaving smoothly with respect to type precision.<\/jats:p>","DOI":"10.1145\/3586036","type":"journal-article","created":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:06:02Z","timestamp":1680815162000},"page":"256-285","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A Gradual Probabilistic Lambda Calculus"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3968-6201","authenticated-orcid":false,"given":"Wenjia","family":"Ye","sequence":"first","affiliation":[{"name":"University of Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5315-0198","authenticated-orcid":false,"given":"Mat\u00edas","family":"Toro","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0217-6483","authenticated-orcid":false,"given":"Federico","family":"Olmedo","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,4,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919)","author":"Avanzini Martin","year":"2021","unstructured":"Martin Avanzini , Ugo Dal Lago , and Alexis Ghyselen . 2021 . Type-Based Complexity Analysis of Probabilistic Functional Programs . In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919) . IEEE Press, Article 41, 13 pages. Martin Avanzini, Ugo Dal Lago, and Alexis Ghyselen. 2021. Type-Based Complexity Analysis of Probabilistic Functional Programs. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919). IEEE Press, Article 41, 13 pages."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 2020 Symposium on Logic in Computer Science (LICS","author":"de Amorim Arthur Azevedo","year":"2020","unstructured":"Arthur Azevedo de Amorim , Matt Fredrikson , and Limin Jia . 2020 . Reconciling Noninterference and Gradual Typing . In Proceedings of the 2020 Symposium on Logic in Computer Science (LICS 2020). Arthur Azevedo de Amorim, Matt Fredrikson, and Limin Jia. 2020. Reconciling Noninterference and Gradual Typing. In Proceedings of the 2020 Symposium on Logic in Computer Science (LICS 2020)."},{"key":"e_1_2_1_3_1","first-page":"1","article-title":"Gradual Type-and-Effect Systems","volume":"26","author":"Schwerter Felipe Ba\u00f1ados","year":"2016","unstructured":"Felipe Ba\u00f1ados Schwerter , Ronald Garcia , and \u00c9ric Tanter . 2016 . Gradual Type-and-Effect Systems . Journal of Functional Programming , 26 (2016), Sept. , 19: 1 \u2013 19 :69. Felipe Ba\u00f1ados Schwerter, Ronald Garcia, and \u00c9ric Tanter. 2016. Gradual Type-and-Effect Systems. Journal of Functional Programming, 26 (2016), Sept., 19:1\u201319:69.","journal-title":"Journal of Functional Programming"},{"key":"e_1_2_1_4_1","volume-title":"Formal Certification of Code-Based Cryptographic Proofs. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201909)","author":"Barthe Gilles","year":"2009","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , and Santiago Zanella-B\u00e9guelin . 2009 . Formal Certification of Code-Based Cryptographic Proofs. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201909) . ACM, New York. 90\u2013101. Gilles Barthe, Benjamin Gr\u00e9goire, and Santiago Zanella-B\u00e9guelin. 2009. Formal Certification of Code-Based Cryptographic Proofs. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201909). ACM, New York. 90\u2013101."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the ACM on Programming Languages, 1, ICFP","author":"Castagna Giuseppe","year":"2017","unstructured":"Giuseppe Castagna and Victor Lanvin . 2017 . Gradual Typing with Union and Intersection Types . Proceedings of the ACM on Programming Languages, 1, ICFP (2017), Sept., 41:1\u201341:28. Giuseppe Castagna and Victor Lanvin. 2017. Gradual Typing with Union and Intersection Types. Proceedings of the ACM on Programming Languages, 1, ICFP (2017), Sept., 41:1\u201341:28."},{"key":"e_1_2_1_6_1","volume-title":"Siek","author":"Castagna Giuseppe","year":"2019","unstructured":"Giuseppe Castagna , Victor Lanvin , Tommaso Petrucciani , and Jeremy G . Siek . 2019 . Gradual typing: a new perspective. 16:1\u201316:32. Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek. 2019. Gradual typing: a new perspective. 16:1\u201316:32."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 9th Joint Meeting on Foundations of Software Engineering (ESEC\/FSE","author":"Claret Guillaume","year":"2013","unstructured":"Guillaume Claret , Sriram K. Rajamani , Aditya V. Nori , Andrew D. Gordon , and Johannes Borgstr\u00f6m . 2013 . Bayesian Inference using Data Flow Analysis . In Proceedings of the 9th Joint Meeting on Foundations of Software Engineering (ESEC\/FSE 2013). ACM, 92\u2013102. Guillaume Claret, Sriram K. Rajamani, Aditya V. Nori, Andrew D. Gordon, and Johannes Borgstr\u00f6m. 2013. Bayesian Inference using Data Flow Analysis. In Proceedings of the 9th Joint Meeting on Foundations of Software Engineering (ESEC\/FSE 2013). ACM, 92\u2013102."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.02.001"},{"key":"e_1_2_1_9_1","volume-title":"abs\/1103.4577","author":"Deng Yuxin","year":"2011","unstructured":"Yuxin Deng and Wenjie Du. 2011. Logical , Metric, and Algorithmic Characterisations of Probabilistic Bisimulation . CoRR , abs\/1103.4577 ( 2011 ), arXiv:1103.4577. arxiv:1103.4577 Yuxin Deng and Wenjie Du. 2011. Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation. CoRR, abs\/1103.4577 (2011), arXiv:1103.4577. arxiv:1103.4577"},{"key":"e_1_2_1_10_1","volume-title":"International Workshop on Scripts to Programs.","author":"Disney Tim","year":"2011","unstructured":"Tim Disney and Cormac Flanagan . 2011 . Gradual information flow typing . In International Workshop on Scripts to Programs. Tim Disney and Cormac Flanagan. 2011. Gradual information flow typing. In International Workshop on Scripts to Programs."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158147"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 26th Computer Security Foundations Symposium (CSF). 224\u2013239","author":"Fennell Luminous","year":"2013","unstructured":"Luminous Fennell and Peter Thiemann . 2013 . Gradual Security Typing with References . In Proceedings of the 26th Computer Security Foundations Symposium (CSF). 224\u2013239 . Luminous Fennell and Peter Thiemann. 2013. Gradual Security Typing with References. In Proceedings of the 26th Computer Security Foundations Symposium (CSF). 224\u2013239."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 18th ACM SIGPLAN International Conference on Functional programming. 417\u2013428","author":"Garcia Ronald","year":"2013","unstructured":"Ronald Garcia . 2013 . Calculating threesomes, with blame . In Proceedings of the 18th ACM SIGPLAN International Conference on Functional programming. 417\u2013428 . Ronald Garcia. 2013. Calculating threesomes, with blame. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional programming. 417\u2013428."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL","author":"Garcia Ronald","year":"2016","unstructured":"Ronald Garcia , Alison M. Clark , and \u00c9ric Tanter . 2016 . Abstracting Gradual Typing . In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), Rastislav Bod\u00edk and Rupak Majumdar (Eds.). ACM Press, St Petersburg, FL, USA. 429\u2013442. See erratum: https:\/\/www.cs.ubc.ca\/ rxg\/agt-erratum.pdf. Ronald Garcia, Alison M. Clark, and \u00c9ric Tanter. 2016. Abstracting Gradual Typing. In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), Rastislav Bod\u00edk and Rupak Majumdar (Eds.). ACM Press, St Petersburg, FL, USA. 429\u2013442. See erratum: https:\/\/www.cs.ubc.ca\/ rxg\/agt-erratum.pdf."},{"key":"e_1_2_1_16_1","volume-title":"Probabilistic Machine Learning and Artificial Intelligence. Nature, 521, 7553","author":"Ghahramani Zoubin","year":"2015","unstructured":"Zoubin Ghahramani . 2015. Probabilistic Machine Learning and Artificial Intelligence. Nature, 521, 7553 ( 2015 ), 452\u2013459. Zoubin Ghahramani. 2015. Probabilistic Machine Learning and Artificial Intelligence. Nature, 521, 7553 (2015), 452\u2013459."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90070-9"},{"key":"e_1_2_1_18_1","volume-title":"Tenenbaum","author":"Goodman Noah D.","year":"2008","unstructured":"Noah D. Goodman , Vikash K. Mansinghka , Daniel Roy , Keith Bonawitz , and Joshua B . Tenenbaum . 2008 . Church : A Language for Generative Models. In Proceedings of the Twenty-Fourth Conference on Uncertainty in Artificial Intelligence (UAI\u201908). AUAI Press , 220\u2013229. isbn:0974903949 Noah D. Goodman, Vikash K. Mansinghka, Daniel Roy, Keith Bonawitz, and Joshua B. Tenenbaum. 2008. Church: A Language for Generative Models. In Proceedings of the Twenty-Fourth Conference on Uncertainty in Artificial Intelligence (UAI\u201908). AUAI Press, 220\u2013229. isbn:0974903949"},{"key":"e_1_2_1_19_1","unstructured":"Noah D Goodman and Andreas Stuhlm\u00fcller. 2014. The Design and Implementation of Probabilistic Programming Languages. http:\/\/dippl.org Accessed: 2022-10-17. \t\t\t\t  Noah D Goodman and Andreas Stuhlm\u00fcller. 2014. The Design and Implementation of Probabilistic Programming Languages. http:\/\/dippl.org Accessed: 2022-10-17."},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the on Future of Software Engineering, FOSE","author":"Gordon Andrew D.","year":"2014","unstructured":"Andrew D. Gordon , Thomas A. Henzinger , Aditya V. Nori , and Sriram K. Rajamani . 2014. Probabilistic programming . In Proceedings of the on Future of Software Engineering, FOSE 2014 . ACM, 167\u2013181. Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. 2014. Probabilistic programming. In Proceedings of the on Future of Software Engineering, FOSE 2014. ACM, 167\u2013181."},{"key":"e_1_2_1_21_1","unstructured":"David Herman Aaron Tomb and Cormac Flanagan. 2007. Space-efficient gradual typing. In In Trends in Functional Programming (TFP. \t\t\t\t  David Herman Aaron Tomb and Cormac Flanagan. 2007. Space-efficient gradual typing. In In Trends in Functional Programming (TFP."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_2_1_23_1","volume-title":"d. S. Oliveira","author":"Huang Xuejing","year":"2020","unstructured":"Xuejing Huang and Bruno C . d. S. Oliveira . 2020 . A Type-Directed Operational Semantics For a Calculus with a Merge Operator. In ECOOP. Xuejing Huang and Bruno C. d. S. Oliveira. 2020. A Type-Directed Operational Semantics For a Calculus with a Merge Operator. In ECOOP."},{"key":"e_1_2_1_24_1","volume-title":"Jafery and Jana Dunfield","author":"Khurram","year":"2017","unstructured":"Khurram A. Jafery and Jana Dunfield . 2017 . Sums of Uncertainty: Refinements Go Gradual . 804\u2013817. Khurram A. Jafery and Jana Dunfield. 2017. Sums of Uncertainty: Refinements Go Gradual. 804\u2013817."},{"key":"e_1_2_1_25_1","volume-title":"Fourth Annual Symposium on Logic in Computer Science, 186\u2013195","author":"Jones C.","unstructured":"C. Jones and Gordon D. Plotkin . 1989. A probabilistic powerdomain of evaluations. [1989] Proceedings . Fourth Annual Symposium on Logic in Computer Science, 186\u2013195 . C. Jones and Gordon D. Plotkin. 1989. A probabilistic powerdomain of evaluations. [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 186\u2013195."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_19"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3293605","article-title":"Probabilistic Termination by Monadic Affine Sized Typing","volume":"41","author":"Lago Ugo Dal","year":"2017","unstructured":"Ugo Dal Lago and Charles Grellois . 2017 . Probabilistic Termination by Monadic Affine Sized Typing . ACM Transactions on Programming Languages and Systems (TOPLAS) , 41 (2017), 1 \u2013 65 . Ugo Dal Lago and Charles Grellois. 2017. Probabilistic Termination by Monadic Affine Sized Typing. ACM Transactions on Programming Languages and Systems (TOPLAS), 41 (2017), 1 \u2013 65.","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/2012012"},{"key":"e_1_2_1_29_1","volume-title":"Probabilistic operational semantics for the lambda calculus. ArXiv, abs\/1104.0195","author":"Lago Ugo Dal","year":"2012","unstructured":"Ugo Dal Lago and Margherita Zorzi . 2012. Probabilistic operational semantics for the lambda calculus. ArXiv, abs\/1104.0195 ( 2012 ). Ugo Dal Lago and Margherita Zorzi. 2012. Probabilistic operational semantics for the lambda calculus. ArXiv, abs\/1104.0195 (2012)."},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 20th International Conference on Artificial Intelligence and Statistics, AISTATS 2017","volume":"1348","author":"Le Tuan Anh","year":"2017","unstructured":"Tuan Anh Le , Atilim Gunes Baydin , and Frank D. Wood . 2017. Inference Compilation and Universal Probabilistic Programming . In Proceedings of the 20th International Conference on Artificial Intelligence and Statistics, AISTATS 2017 , 20-22 April 2017 , Fort Lauderdale, FL, USA, Aarti Singh and Xiaojin (Jerry) Zhu (Eds.) (Proceedings of Machine Learning Research , Vol. 54). PMLR, 1338\u2013 1348 . http:\/\/proceedings.mlr.press\/v54\/le17a.html Tuan Anh Le, Atilim Gunes Baydin, and Frank D. Wood. 2017. Inference Compilation and Universal Probabilistic Programming. In Proceedings of the 20th International Conference on Artificial Intelligence and Statistics, AISTATS 2017, 20-22 April 2017, Fort Lauderdale, FL, USA, Aarti Singh and Xiaojin (Jerry) Zhu (Eds.) (Proceedings of Machine Learning Research, Vol. 54). PMLR, 1338\u20131348. http:\/\/proceedings.mlr.press\/v54\/le17a.html"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Nico Lehmann and \u00c9ric Tanter. 2017. Gradual Refinement Types. 775\u2013788. \t\t\t\t  Nico Lehmann and \u00c9ric Tanter. 2017. Gradual Refinement Types. 775\u2013788.","DOI":"10.1145\/3093333.3009856"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Meven Lennon-Bertrand Kenji Maillard Nicolas Tabareau and \u00c9ric Tanter. 2022. Gradualizing the Calculus of Inductive Constructions. ACM Transactions on Programming Languages and Systems To appear. To be presented at POPL\u201922. \t\t\t\t  Meven Lennon-Bertrand Kenji Maillard Nicolas Tabareau and \u00c9ric Tanter. 2022. Gradualizing the Calculus of Inductive Constructions. ACM Transactions on Programming Languages and Systems To appear. To be presented at POPL\u201922.","DOI":"10.1145\/3495528"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the ACM on Programming Languages, 5, OOPSLA","author":"Malewski Stefan","year":"2021","unstructured":"Stefan Malewski , Michael Greenberg , and \u00c9ric Tanter . 2021 . Gradually Structured Data . Proceedings of the ACM on Programming Languages, 5, OOPSLA (2021), Nov., 126:1\u2013126:28. Stefan Malewski, Michael Greenberg, and \u00c9ric Tanter. 2021. Gradually Structured Data. Proceedings of the ACM on Programming Languages, 5, OOPSLA (2021), Nov., 126:1\u2013126:28."},{"key":"e_1_2_1_34_1","volume-title":"Randomized Algorithms","author":"Motwani Rajeev","unstructured":"Rajeev Motwani and Prabhakar Raghavan . 1995. Randomized Algorithms . Cambridge University Press . Rajeev Motwani and Prabhakar Raghavan. 1995. Randomized Algorithms. Cambridge University Press."},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Max S. New Daniel R. Licata and Amal Ahmed. 2019. Gradual Type Theory. 15:1\u201315:31. \t\t\t\t  Max S. New Daniel R. Licata and Amal Ahmed. 2019. Gradual Type Theory. 15:1\u201315:31.","DOI":"10.1145\/3290328"},{"key":"e_1_2_1_36_1","volume-title":"ILP 2010","author":"Pfeffer Avi","year":"2010","unstructured":"Avi Pfeffer . 2010 . Practical Probabilistic Programming. In Inductive Logic Programming - 20th International Conference , ILP 2010 , Florence, Italy , June 27-30, 2010. Revised Papers, Paolo Frasconi and Francesca A. Lisi (Eds.) (Lecture Notes in Computer Science, Vol. 6489). Springer, 2\u20133. Avi Pfeffer. 2010. Practical Probabilistic Programming. In Inductive Logic Programming - 20th International Conference, ILP 2010, Florence, Italy, June 27-30, 2010. Revised Papers, Paolo Frasconi and Francesca A. Lisi (Eds.) (Lecture Notes in Computer Science, Vol. 6489). Springer, 2\u20133."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485488"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL","year":"2017","unstructured":"2017. Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017 ). ACM Press, Paris, France. 2017. Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017). ACM Press, Paris, France."},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the 46th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL","year":"2019","unstructured":"2019. Proceedings of the 46th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2019 ). 2019. Proceedings of the 46th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2019)."},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Norman Ramsey and Avi Pfeffer. 2002. Stochastic lambda calculus and monads of probability distributions. In POPL \u201902. \t\t\t\t  Norman Ramsey and Avi Pfeffer. 2002. Stochastic lambda calculus and monads of probability distributions. In POPL \u201902.","DOI":"10.1145\/503272.503288"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP\u201910)","author":"Reed Jason","unstructured":"Jason Reed and Benjamin C. Pierce . 2010. Distance Makes the Types Grow Stronger: A Calculus for Differential Privacy . In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP\u201910) . ACM, 157\u2013168. Jason Reed and Benjamin C. Pierce. 2010. Distance Makes the Types Grow Stronger: A Calculus for Differential Privacy. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP\u201910). ACM, 157\u2013168."},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Amr Sabry and Matthias Felleisen. 1993. Reasoning about Programs in Continuation-Passing Style. In LISP AND SYMBOLIC COMPUTATION. 288\u2013298. \t\t\t\t  Amr Sabry and Matthias Felleisen. 1993. Reasoning about Programs in Continuation-Passing Style. In LISP AND SYMBOLIC COMPUTATION. 288\u2013298.","DOI":"10.1145\/141478.141563"},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Nasser Saheb-Djahromi. 1978. Probabilistic LCF. In MFCS. \t\t\t\t  Nasser Saheb-Djahromi. 1978. Probabilistic LCF. In MFCS.","DOI":"10.1007\/3-540-08921-7_92"},{"key":"e_1_2_1_44_1","first-page":"250","article-title":"Probabilistic Simulations for Probabilistic Processes","volume":"2","author":"Segala Roberto","year":"1995","unstructured":"Roberto Segala and Nancy A. Lynch . 1995 . Probabilistic Simulations for Probabilistic Processes . Nord. J. Comput. , 2 , 2 (1995), 250 \u2013 273 . Roberto Segala and Nancy A. Lynch. 1995. Probabilistic Simulations for Probabilistic Processes. Nord. J. Comput., 2, 2 (1995), 250\u2013273.","journal-title":"Nord. J. Comput."},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the Scheme and Functional Programming Workshop. 81\u201392","author":"Siek Jeremy","year":"2006","unstructured":"Jeremy Siek and Walid Taha . 2006 . Gradual Typing for Functional Languages . In Proceedings of the Scheme and Functional Programming Workshop. 81\u201392 . Jeremy Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Proceedings of the Scheme and Functional Programming Workshop. 81\u201392."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737968"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_1_48_1","unstructured":"Jeremy G. Siek Ronald Garcia and Walid Taha. 2009. Exploring the Design Space of Higher-Order Casts. In ESOP. \t\t\t\t  Jeremy G. Siek Ronald Garcia and Walid Taha. 2009. Exploring the Design Space of Higher-Order Casts. In ESOP."},{"key":"e_1_2_1_49_1","volume-title":"Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)","volume":"293","author":"Siek Jeremy G.","year":"2015","unstructured":"Jeremy G. Siek , Michael M. Vitousek , Matteo Cimini , and John Tang Boyland . 2015 . Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs) , Vol. 32). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Asilomar, California, USA. 274\u2013 293 . Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 32). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Asilomar, California, USA. 274\u2013293."},{"key":"e_1_2_1_50_1","unstructured":"Jeremy G. Siek Michael M. Vitousek Matteo Cimini Sam Tobin-Hochstadt and Ronald Garcia. 2015. Monotonic References for Efficient Gradual Typing. In ESOP. \t\t\t\t  Jeremy G. Siek Michael M. Vitousek Matteo Cimini Sam Tobin-Hochstadt and Ronald Garcia. 2015. Monotonic References for Efficient Gradual Typing. In ESOP."},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 27th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA","author":"Takikawa Asumu","year":"2012","unstructured":"Asumu Takikawa , T. Stephen Strickland , Christos Dimoulas , Sam Tobin-Hochstadt , and Matthias Felleisen . 2012 . Gradual Typing for First-Class Classes . In Proceedings of the 27th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2012). ACM Press, Tucson, AZ, USA. 793\u2013810. Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. 2012. Gradual Typing for First-Class Classes. In Proceedings of the 27th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2012). ACM Press, Tucson, AZ, USA. 793\u2013810."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229061"},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the 24th Static Analysis Symposium (SAS 2017)","volume":"404","author":"Mat\u00edas","unstructured":"Mat\u00edas Toro and \u00c9ric Tanter. 2017. A Gradual Interpretation of Union Types . In Proceedings of the 24th Static Analysis Symposium (SAS 2017) (Lecture Notes in Computer Science , Vol. 10422). Springer-Verlag, New York City, NY, USA. 382\u2013 404 . Mat\u00edas Toro and \u00c9ric Tanter. 2017. A Gradual Interpretation of Union Types. In Proceedings of the 24th Static Analysis Symposium (SAS 2017) (Lecture Notes in Computer Science, Vol. 10422). Springer-Verlag, New York City, NY, USA. 382\u2013404."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102496"},{"key":"e_1_2_1_55_1","volume-title":"Blei","author":"Tran Dustin","year":"2017","unstructured":"Dustin Tran , Matthew D. Hoffman , Rif A. Saurous , Eugene Brevdo , Kevin Murphy , and David M . Blei . 2017 . Deep Probabilistic Programming. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. OpenReview .net. https:\/\/openreview.net\/forum?id=Hy6b4Pqee Dustin Tran, Matthew D. Hoffman, Rif A. Saurous, Eugene Brevdo, Kevin Murphy, and David M. Blei. 2017. Deep Probabilistic Programming. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. OpenReview.net. https:\/\/openreview.net\/forum?id=Hy6b4Pqee"},{"key":"e_1_2_1_56_1","volume-title":"An Introduction to Probabilistic Programming. CoRR, abs\/1809.10756","author":"van de Meent Jan-Willem","year":"2018","unstructured":"Jan-Willem van de Meent , Brooks Paige , Hongseok Yang , and Frank Wood . 2018. An Introduction to Probabilistic Programming. CoRR, abs\/1809.10756 ( 2018 ), arXiv:1809.10756. arxiv:1809.10756 Jan-Willem van de Meent, Brooks Paige, Hongseok Yang, and Frank Wood. 2018. An Introduction to Probabilistic Programming. CoRR, abs\/1809.10756 (2018), arXiv:1809.10756. arxiv:1809.10756"},{"key":"e_1_2_1_57_1","volume-title":"Proceedings of the 18th European Symposium on Programming Languages and Systems (ESOP","volume":"16","author":"Wadler Philip","year":"2009","unstructured":"Philip Wadler and Robert Bruce Findler . 2009 . Well-Typed Programs Can\u2019t Be Blamed . In Proceedings of the 18th European Symposium on Programming Languages and Systems (ESOP 2009), Giuseppe Castagna (Ed.) (Lecture Notes in Computer Science , Vol. 5502). Springer-Verlag, York, UK. 1\u2013 16 . Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can\u2019t Be Blamed. In Proceedings of the 18th European Symposium on Programming Languages and Systems (ESOP 2009), Giuseppe Castagna (Ed.) (Lecture Notes in Computer Science, Vol. 5502). Springer-Verlag, York, UK. 1\u201316."},{"key":"e_1_2_1_58_1","volume-title":"d. S. Oliveira, and Xuejing Huang","author":"Ye Wenjia","year":"2021","unstructured":"Wenjia Ye , Bruno C. d. S. Oliveira, and Xuejing Huang . 2021 . Type-Directed Operational Semantics for Gradual Typing. In ECOOP. Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang. 2021. Type-Directed Operational Semantics for Gradual Typing. In ECOOP."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586036","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3586036","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:10Z","timestamp":1750178770000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586036"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,6]]},"references-count":58,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2023,4,6]]}},"alternative-id":["10.1145\/3586036"],"URL":"https:\/\/doi.org\/10.1145\/3586036","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,6]]},"assertion":[{"value":"2023-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}