{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:51:59Z","timestamp":1743061919431,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452308"},{"type":"electronic","value":"9783030452315"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We propose a \u201cCurry-style\u201d semantics of programs in which a nominal labelled transition system of types, characterizing observable behaviour, is overlaid on a nominal LTS of untyped computation. This leads to a notion of program equivalence as typed bisimulation.<\/jats:p><jats:p>Our semantics reflects the role of types as hiding operators, firstly via an axiomatic characterization of \u201cparallel composition with hiding\u201d which yields a general technique for establishing congruence results for typed bisimulation, and secondly via an example which captures the hiding of implementations in abstract data types: a typed bisimulation for the (Curry-style) lazy<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda \\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u03bb<\/mml:mi><mml:mi>\u03bc<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus with polymorphic types. This is built on an abstract machine for CPS evaluation of<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda \\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u03bb<\/mml:mi><mml:mi>\u03bc<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-terms: we first give a basic typing system for this LTS which characterizes acyclicity of the environment and local control flow, and then refine this to a polymorphic typing system which uses equational constraints on instantiated type variables, inferred from observable interaction, to capture behaviour at polymorphic and abstract types.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_22","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"422-441","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Curry-style Semantics of Interaction: From Untyped to Second-Order Lazy $$\\lambda \\mu $$-Calculus"],"prefix":"10.1007","author":[{"given":"James","family":"Laird","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"22_CR1","unstructured":"S.\u00a0Abramsky. The lazy $$\\lambda $$-calculus. In D.\u00a0Turner, editor, Research Topics in Functional Programming, pages 65\u2013117. Addison Wesley, 1990."},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"S.\u00a0Abramsky, R.\u00a0Jagadeesan, and P.\u00a0Malacaria. Full abstraction for PCF. Information and Computation, 163:409\u2013470, 2000.","DOI":"10.1006\/inco.2000.2930"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"M.\u00a0Berger, K.\u00a0Honda, and N.\u00a0Yoshida. Sequentiality and the $$\\pi $$-calculus. In Proceedings of TLCA 2001, volume 2044 of Lecture Notes in Computer Science. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45413-6_7"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"M.\u00a0Berger, K.\u00a0Honda, and N.\u00a0Yoshida. Genericity and the $$\\pi $$-calculus. Acta Informatica, 42, 2005.","DOI":"10.1007\/s00236-005-0175-1"},{"key":"22_CR5","unstructured":"M.\u00a0Berger, K.\u00a0Honda, and N.\u00a0Yoshida. Process types as a descriptive tool for interaction: Control and the $$\\pi $$-calculus. In Proceedings of the Rewriting and Typed Lambda-calculi - joint international conference, 2014."},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"D.\u00a0R.\u00a0Ghica and N.\u00a0Tzevelekos. System level game semantics. Proceedings of MFPS XXVIII, ENTCS volume 286, pages 191 \u2013211. 2012.","DOI":"10.1016\/j.entcs.2012.08.013"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard. Linear logic. Theoretical Computer Science, 50, 1987.","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"22_CR8","unstructured":"D.\u00a0Hughes. Games and definability for System F. In Proceedings of the Twelfth International syposium on Logic in Computer Science, LICS \u201997. IEEE Computer Society Press, 1997."},{"key":"22_CR9","unstructured":"J.\u00a0M.\u00a0E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II and III. Information and Computation, 163:285\u2013408, 2000."},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"A.\u00a0Igurashi and N.\u00a0Kobayashi. A generic type system for the $$\\pi $$-calculus. Theoretical Computer Science, 311:121\u2013163, 2004.","DOI":"10.1016\/S0304-3975(03)00325-6"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Vladimir\u00a0N. Krupski. The single-conclusion proof logic and inference rules specification. Annals of Pure and Applied Logic, 113:181 \u2013 206, 2002.","DOI":"10.1016\/S0168-0072(01)00058-6"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"J.\u00a0Laird. A fully abstract trace semantics for general references. In 34th ICALP, volume 4596 of LNCS, pages 667\u2013679. Springer, 2007.","DOI":"10.1007\/978-3-540-73420-8_58"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"J.\u00a0Laird. Game semantics of call-by-value polymorphism. In Proceedings of ICALP \u201910, number 6198 in LNCS. Springer-Verlag, 2010.","DOI":"10.1007\/978-3-642-14162-1_16"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"J.\u00a0Laird. Game semantics for a polymorphic programming language. Journal of the ACM, 60(4), 2013.","DOI":"10.1145\/2508028.2505986"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"S.\u00a0B. Lassen and P.\u00a0B. Levy. Typed normal form bisimulation. In Proceedings 16th EACSL Conference on Computer Science and Logic, number 4646 in LNCS, pages 283\u2013297, 2007.","DOI":"10.1007\/978-3-540-74915-8_23"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Joachim\u00a0De Lataillade. Curry-style type isomorphisms and game semantics. MSCS, 18:647\u2013692, 2008.","DOI":"10.1017\/S0960129508006828"},{"key":"22_CR17","unstructured":"P.\u00a0B. Levy and S.\u00a0Lassen. Typed normal form bisimulation for parametric polymorphism. In Proceedings of LICS 2008, pages 341\u2013552. IEEE press, 2008."},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Paul Levy and Sam Staton. Transition systems over games. In CSL-LICS \u201914. ACM Press, 2014.","DOI":"10.1145\/2603088.2603150"},{"key":"22_CR19","unstructured":"G.\u00a0Longo. Set-theoretical models of lambda calculus: Theories, expansions and isomorphisms. Annals of Pure and Applied Logic, 24:153\u2013188, 1983."},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"J.\u00a0Mitchell and G.\u00a0Plotkin. Abstract types have existential type. ACM transactions on Programming Languages and Systems, 10(3):470\u2013502, 1988.","DOI":"10.1145\/44501.45065"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"M.\u00a0Parigot. $$\\lambda \\mu $$ calculus: an algorithmic interpretation of classical natural deduction. In Proc. International Conference on Logic Programming and Automated Reasoning, pages 190\u2013201. Springer, 1992.","DOI":"10.1007\/BFb0013061"},{"key":"22_CR22","unstructured":"Joachim Parrow, Johannes Borgstr\u00f6m, Lars-Henrik Eriksson, Ramunas Gutkovas, and Tjark Weber. Modal Logics for Nominal Transition Systems. In 26th International Conference on Concurrency Theory (CONCUR 2015), volume\u00a042, pages 198\u2013211, 2015."},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"A.\u00a0M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013.","DOI":"10.1017\/CBO9781139084673"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"J.\u00a0C. Reynolds. Towards a theory of type structure. In Proceedings of the Programming Symposium, Paris 1974, number\u00a019 in LNCS. Springer, 1974.","DOI":"10.1007\/3-540-06859-7_148"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"D.\u00a0Sangiorgi. The lazy $$\\lambda $$-calculus in a concurrency scenario. Information and Computation, 111:120 \u2013153, 1994.","DOI":"10.1006\/inco.1994.1042"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"M.\u00a0Smyth and G.\u00a0Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal on Computing, 11(4):761\u2013783, 1982.","DOI":"10.1137\/0211062"},{"key":"22_CR27","unstructured":"N.\u00a0Tzevelekos and G.\u00a0Jaber. Trace semantics for polymorphic references. In Proc. LICS\u201916, pages 585\u2013594. ACM, 2016."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,21]],"date-time":"2022-10-21T15:49:22Z","timestamp":1666367362000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","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":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/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":"98","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":"31","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":"32% - 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","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":"12","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)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}