{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T01:24:11Z","timestamp":1778635451278,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,1,17]],"date-time":"2021-01-17T00:00:00Z","timestamp":1610841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,1,17]]},"DOI":"10.1145\/3437992.3439914","type":"proceedings-article","created":{"date-parts":[[2021,1,20]],"date-time":"2021-01-20T23:11:11Z","timestamp":1611184271000},"page":"178-198","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Machine-checked semantic session typing"],"prefix":"10.1145","author":[{"given":"Jonas Kastberg","family":"Hinrichsen","sequence":"first","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dani\u00ebl","family":"Louwrink","sequence":"additional","affiliation":[{"name":"University of Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Netherlands \/ Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jesper","family":"Bengtson","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,20]]},"reference":[{"key":"e_1_3_2_1_2_1","volume-title":"Wang","author":"Ahmed Amal","year":"2010"},{"key":"e_1_3_2_1_3_1","volume-title":"McAllester","author":"Appel Andrew W.","year":"2001"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1145\/1190216.1190235","article-title":"A very modal model of a modern, major, general type system","author":"Appel Andrew W.","year":"2007","journal-title":"POPL."},{"key":"e_1_3_2_1_5_1","unstructured":"Stephanie Balzer and Frank Pfenning. 2017. Manifest Sharing with Session Types. PACMPL 1 ICFP ( 2017 ) 37 : 1-37 : 29. htps:\/\/doi.org\/10. 1145\/3110281 Stephanie Balzer and Frank Pfenning. 2017. Manifest Sharing with Session Types. PACMPL 1 ICFP ( 2017 ) 37 : 1-37 : 29. htps:\/\/doi.org\/10. 1145\/3110281"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_22"},{"key":"e_1_3_2_1_7_1","volume-title":"Undecidability of asynchronous session subtyping. Information and Computation 256 ( 2017 ), 300-320. htps:\/\/doi.org\/10.1016\/j.ic","author":"Bravetti Mario","year":"2017"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0285-y"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_17"},{"key":"e_1_3_2_1_12_1","volume-title":"Gay","author":"Dardha Ornela","year":"2018"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2370776.2370794"},{"key":"e_1_3_2_1_14_1","first-page":"71","article-title":"Logical StepIndexed Logical Relations","author":"Dreyer Derek","year":"2009","journal-title":"LICS."},{"key":"e_1_3_2_1_15_1","unstructured":"Derek Dreyer Amin Timany Robbert Krebbers Lars Birkedal and Ralf Jung. 2019. What Type Soundness Theorem Do You Really Want to Prove? SIGPLAN blog post available at htps:\/\/blog.sigplan.org\/ 2019 \/10\/17\/what-type-soundness-theoremdo-you-really-want-to-prove\/. Derek Dreyer Amin Timany Robbert Krebbers Lars Birkedal and Ralf Jung. 2019. What Type Soundness Theorem Do You Really Want to Prove? SIGPLAN blog post available at htps:\/\/blog.sigplan.org\/ 2019 \/10\/17\/what-type-soundness-theoremdo-you-really-want-to-prove\/."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Dan Frumin Robbert Krebbers and Lars Birkedal. 2020. Compositional Non-Interference for Fine-Grained Concurrent Programs. To appear in S&P' 21. Dan Frumin Robbert Krebbers and Lars Birkedal. 2020. Compositional Non-Interference for Fine-Grained Concurrent Programs. To appear in S&P' 21.","DOI":"10.1109\/SP40001.2021.00003"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Simon J. Gay. 2008. Bounded polymorphism in session types. MSCS 18 5 ( 2008 ) 895-930. htps:\/\/doi.org\/10.1017\/S0960129508006944 Simon J. Gay. 2008. Bounded polymorphism in session types. MSCS 18 5 ( 2008 ) 895-930. htps:\/\/doi.org\/10.1017\/S0960129508006944","DOI":"10.1017\/S0960129508006944"},{"key":"e_1_3_2_1_19_1","volume-title":"A List of Successes That Can Change the World-Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. 95-108. htps: \/\/doi.org\/10.1007\/978-3-319-30936-1_5","author":"Gay Simon J."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_3_2_1_21_1","volume-title":"Vasconcelos","author":"Gay Simon J.","year":"2020"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Paolo G. Giarrusso L\u00e9o Stefanesco Amin Timany Lars Birkedal and Robbert Krebbers. 2020. Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. PACMPL 4 ICFP ( 2020 ) 114 : 1-114 : 29. htps:\/\/doi.org\/10.1145\/3408996 Paolo G. Giarrusso L\u00e9o Stefanesco Amin Timany Lars Birkedal and Robbert Krebbers. 2020. Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. PACMPL 4 ICFP ( 2020 ) 114 : 1-114 : 29. htps:\/\/doi.org\/10.1145\/3408996","DOI":"10.1145\/3408996"},{"key":"e_1_3_2_1_23_1","unstructured":"Jonas Kastberg Hinrichsen Jesper Bengtson and Robbert Krebbers. 2020. Actris 2.0: Asynchronous session-type based reasoning in separation logic. ( 2020 ). Manuscript in preparation. Jonas Kastberg Hinrichsen Jesper Bengtson and Robbert Krebbers. 2020. Actris 2.0: Asynchronous session-type based reasoning in separation logic. ( 2020 ). Manuscript in preparation."},{"key":"e_1_3_2_1_24_1","volume-title":"Actris: Session-type based reasoning in separation logic. PACMPL 4, POPL ( 2020 ), 6 : 1-6 : 30. htps:\/\/doi.org\/10.1145\/3371074","author":"Hinrichsen Jonas Kastberg","year":"2020"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Jonas Kastberg Hinrichsen Dani\u00ebl Louwrink Robbert Krebbers and Jesper Bengtson. 2021. Coq Mechanization of ?Machine-Checked Semantic Session Typing?. Archived version at htps:\/\/zenodo.org\/ record\/4322752 latest version at htps:\/\/gitlab.mpi-sws.org\/iris\/actris. Jonas Kastberg Hinrichsen Dani\u00ebl Louwrink Robbert Krebbers and Jesper Bengtson. 2021. Coq Mechanization of ?Machine-Checked Semantic Session Typing?. Archived version at htps:\/\/zenodo.org\/ record\/4322752 latest version at htps:\/\/gitlab.mpi-sws.org\/iris\/actris.","DOI":"10.1145\/3437992.3439914"},{"key":"e_1_3_2_1_26_1","volume-title":"Vasco Thudichum Vasconcelos, and Makoto Kubo","author":"Honda Kohei","year":"1998"},{"key":"e_1_3_2_1_27_1","unstructured":"Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2018. RustBelt: Securing the Foundations of the Rust Programming Language. PACMPL 2 POPL ( 2018 ) 66 : 1-66 : 34. htps:\/\/doi.org\/10. 1145\/3158154 Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2018. RustBelt: Securing the Foundations of the Rust Programming Language. PACMPL 2 POPL ( 2018 ) 66 : 1-66 : 34. htps:\/\/doi.org\/10. 1145\/3158154"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2020. Safe systems programming in Rust: The promise and the challenge. To appear in CACM. Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2020. Safe systems programming in Rust: The promise and the challenge. To appear in CACM.","DOI":"10.1145\/3418295"},{"key":"e_1_3_2_1_29_1","first-page":"256","article-title":"Higher-Order Ghost State","author":"Jung Ralf","year":"2016","journal-title":"ICFP."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris From the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic. JFP 28 ( 2018 ) e20. htps:\/\/doi.org\/10.1017\/S0956796818000151 Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris From the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic. JFP 28 ( 2018 ) e20. htps:\/\/doi.org\/10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: A General Extensible Modal Framework for Interactive Proofs in Separation Logic. PACMPL 2 ICFP ( 2018 ) 77 : 1-77 : 30. htps:\/\/doi.org\/10.1145\/3236772 Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: A General Extensible Modal Framework for Interactive Proofs in Separation Logic. PACMPL 2 ICFP ( 2018 ) 77 : 1-77 : 30. htps:\/\/doi.org\/10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_2_1_34_1","first-page":"205","article-title":"Interactive Proofs in Higher-Order Concurrent Separation Logic","author":"Krebbers Robbert","year":"2017","journal-title":"POPL."},{"key":"e_1_3_2_1_35_1","first-page":"218","article-title":"A relational model of types-and-efects in higher-order concurrent separation logic","author":"Krogh-Jespersen Morten","year":"2017","journal-title":"POPL."},{"key":"e_1_3_2_1_36_1","volume-title":"Session typing and asynchronous subtyping for the higher-order-calculus. Information and Computation 241 ( 2015 ), 227-263. htps:\/\/doi.org\/10.1016\/j.ic","author":"Mostrous Dimitris","year":"2015"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_23"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_27"},{"key":"e_1_3_2_1_39_1","volume-title":"Linear logical relations and observational equivalences for session-based concurrency. Information and Computation 239 ( 2014 ), 254-302. htps:\/\/doi.org\/10.1016\/j.ic","author":"P\u00e9rez Jorge A.","year":"2014"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1145\/53990.54010","article-title":"Higher-Order Abstract Syntax","author":"Pfenning Frank","year":"1988","journal-title":"PLDI."},{"key":"e_1_3_2_1_41_1","volume-title":"Pierce et al","author":"Benjamin","year":"2020"},{"key":"e_1_3_2_1_42_1","first-page":"284","article-title":"Intrinsically-typed definitional interpreters for linear, session-typed languages","author":"Rouvoet Arjen","year":"2020","journal-title":"CPP. ACM"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"crossref","unstructured":"David Swasey Deepak Garg and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns. PACMPL 1 OOPSLA ( 2017 ) 89 : 1-89 : 26. htps:\/\/doi.org\/10.1145\/3133913 David Swasey Deepak Garg and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns. PACMPL 1 OOPSLA ( 2017 ) 89 : 1-89 : 26. htps:\/\/doi.org\/10.1145\/3133913","DOI":"10.1145\/3133913"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_3_2_1_45_1","unstructured":"The Coq-std++ Team. 2020. An extended ?standard library? for Coq. Available online at htps:\/\/gitlab.mpi-sws.org\/iris\/stdpp. The Coq-std++ Team. 2020. An extended ?standard library? for Coq. Available online at htps:\/\/gitlab.mpi-sws.org\/iris\/stdpp."},{"key":"e_1_3_2_1_46_1","first-page":"1","article-title":"Intrinsically-Typed Mechanized Semantics for Session Types","volume":"19","author":"Thiemann Peter","year":"2019","journal-title":"PPDP."},{"key":"e_1_3_2_1_47_1","volume-title":"Vasconcelos","author":"Thiemann Peter","year":"2020"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"crossref","unstructured":"Amin Timany L\u00e9o Stefanesco Morten Krogh-Jespersen and Lars Birkedal. 2018. A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of runST. PACMPL 2 POPL ( 2018 ) 64 : 1-64 : 28. htps:\/\/doi.org\/10.1145\/3158152 Amin Timany L\u00e9o Stefanesco Morten Krogh-Jespersen and Lars Birkedal. 2018. A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of runST. PACMPL 2 POPL ( 2018 ) 64 : 1-64 : 28. htps:\/\/doi.org\/10.1145\/3158152","DOI":"10.1145\/3158152"},{"key":"e_1_3_2_1_49_1","first-page":"273","article-title":"Propositions as sessions","author":"Wadler Philip","year":"2012","journal-title":"ICFP."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"crossref","unstructured":"Andrew K. Wright. 1995. Simple Imperative Polymorphism. Lisp and Symbolic Computation 8 4 ( 1995 ) 343-355. Andrew K. Wright. 1995. Simple Imperative Polymorphism. Lisp and Symbolic Computation 8 4 ( 1995 ) 343-355.","DOI":"10.1007\/BF01018828"}],"event":{"name":"CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Virtual Denmark","acronym":"CPP '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3437992.3439914","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3437992.3439914","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:18Z","timestamp":1750193238000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3437992.3439914"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,17]]},"references-count":49,"alternative-id":["10.1145\/3437992.3439914","10.1145\/3437992"],"URL":"https:\/\/doi.org\/10.1145\/3437992.3439914","relation":{},"subject":[],"published":{"date-parts":[[2021,1,17]]},"assertion":[{"value":"2021-01-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}