{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:18Z","timestamp":1751660538703,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308284"},{"type":"electronic","value":"9783031308291"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T00:00:00Z","timestamp":1682035200000},"content-version":"vor","delay-in-days":110,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Much work has been done to give semantics to probabilistic programming languages. In recent years, most of the semantics used to reason about probabilistic programs fall in two categories: semantics based on Markov kernels and semantics based on linear operators.<\/jats:p><jats:p>Both styles of semantics have found numerous applications in reasoning about probabilistic programs, but they each have their strengths and weaknesses. Though it is believed that there is a connection between them there are no languages that can handle both styles of programming.<\/jats:p><jats:p>In this work we address these questions by defining a two-level calculus and its categorical semantics which makes it possible to program with both kinds of semantics. From the logical side of things we see this language as an alternative resource interpretation of linear logic, where the resource being kept track of is sampling instead of variable use.<\/jats:p>","DOI":"10.1007\/978-3-031-30829-1_5","type":"book-chapter","created":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T19:56:19Z","timestamp":1682020579000},"page":"89-112","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Higher-Order Language for Markov Kernels and Linear Operators"],"prefix":"10.1007","author":[{"given":"Pedro H. Azevedo","family":"de Amorim","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,21]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"de\u00a0Amorim, A.A., Gaboardi, M., Hsu, J., Katsumata, S.y.: Probabilistic relational reasoning via metrics. In: Symposium on Logic in Computer Science (LICS) (2019)","DOI":"10.1109\/LICS.2019.8785715"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Aumann, R.J.: Borel structures for function spaces. Illinois Journal of Mathematics (1961)","DOI":"10.1215\/ijm\/1255631584"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., Fournet, C., Gr\u00e9goire, B., Strub, P.Y., Swamy, N., Zanella-B\u00e9guelin, S.: Probabilistic relational verification for cryptographic implementations. In: Principles of Programming Languages (POPL) (2014)","DOI":"10.1145\/2535838.2535847"},{"key":"5_CR4","unstructured":"Benton, N., Wadler, P.: Linear logic, monads and the lambda calculus. In: Symposium on Logic in Computer Science (LICS) (1996)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Borceux, F.: Handbook of Categorical Algebra: Volume 2, Categories and Structures, vol.\u00a02. Cambridge University Press (1994)","DOI":"10.1017\/CBO9780511525858"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: International Conference on Computer Aided Verification (CAV) (2013)","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Clerc, F., Danos, V., Dahlqvist, F., Garnier, I.: Pointless learning. In: International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) (2017)","DOI":"10.1007\/978-3-662-54458-7_21"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Dahlqvist, F., Kozen, D.: Semantics of higher-order probabilistic programs with conditioning. In: Principles of Programming Languages (POPL) (2019)","DOI":"10.1145\/3371125"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Danos, V., Ehrhard, T.: Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation 209(6), 966\u2013991 (2011)","DOI":"10.1016\/j.ic.2011.02.001"},{"key":"5_CR10","unstructured":"Ehrhard, T.: On the linear structure of cones. In: Logic in Computer Science (LICS) (2020)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Ehrhard, T., Pagani, M., Tasson, C.: Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. In: Principles of Programming Languages (POPL) (2017)","DOI":"10.1145\/3158147"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Fritz, T.: A synthetic approach to markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics 370, 107239 (2020)","DOI":"10.1016\/j.aim.2020.107239"},{"key":"5_CR13","unstructured":"Geoffroy, G.: Extensional denotational semantics of higher-order probabilistic programs, beyond the discrete case (unpublished) (2021)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Goubault-Larrecq, J.: A probabilistic and non-deterministic call-by-push-value language. In: Logic in Computer Science (LICS) (2019)","DOI":"10.1109\/LICS.2019.8785809"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Heunen, C., Kammar, O., Staton, S., Yang, H.: A convenient category for higher-order probability theory. In: Logic in Computer Science (LICS) (2017)","DOI":"10.1109\/LICS.2017.8005137"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Huang, M., Fu, H., Chatterjee, K., Goharshady, A.K.: Modular verification for almost-sure termination of probabilistic programs. Proceedings of the ACM on Programming Languages (OOPSLA) (2019)","DOI":"10.1145\/3360555"},{"key":"5_CR17","unstructured":"Levy, P.B.: Call-by-push-value. Ph.D. thesis (2001)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theoretical Computer Science (1999)","DOI":"10.1016\/S0304-3975(98)00358-2"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"McBride, C., Paterson, R.: Applicative programming with effects. Journal of functional programming 18(1), 1\u201313 (2008)","DOI":"10.1017\/S0956796807006326"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.P.: A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages (POPL) (2017)","DOI":"10.1145\/3158121"},{"key":"5_CR21","unstructured":"Mellies, P.A.: Categorical semantics of linear logic. Panoramas et syntheses 27, 15\u2013215 (2009)"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Scibior, A., Kammar, O., Vakar, M., Staton, S., Yang, H., Cai, Y., Ostermann, K., Moss, S., Heunen, C., Ghahramani, Z.: Denotational validation of higher-order bayesian inference. Proceedings of the ACM on Programming Languages (2018)","DOI":"10.1145\/3158148"},{"key":"5_CR23","unstructured":"Seal, G.J.: Tensors, monads and actions. arXiv preprint arXiv:1205.0101 (2012)"},{"key":"5_CR24","unstructured":"Tasson, C., Ehrhard, T.: Probabilistic call by push value. Logical Methods in Computer Science (2019)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30829-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T19:57:41Z","timestamp":1682020661000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30829-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308284","9783031308291"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30829-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"21 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"85","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}