{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T16:05:20Z","timestamp":1750089920229,"version":"3.41.0"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030780883"},{"type":"electronic","value":"9783030780890"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-78089-0_9","type":"book-chapter","created":{"date-parts":[[2021,6,9]],"date-time":"2021-06-09T14:26:35Z","timestamp":1623248795000},"page":"157-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["$$\\pi $$ with Leftovers: A Mechanisation in Agda"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3268-9338","authenticated-orcid":false,"given":"Uma","family":"Zalakain","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9927-7875","authenticated-orcid":false,"given":"Ornela","family":"Dardha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,8]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.entcs.2007.11.010","volume":"199","author":"R Affeldt","year":"2008","unstructured":"Affeldt, R., Kobayashi, N.: A Coq Library for Verification of Concurrent Programs. Electron. Notes Theor. Comput. Sci. 199, 17\u201332 (2008). https:\/\/doi.org\/10.1016\/j.entcs.2007.11.010","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Allais, G.: Typing with leftovers - a mechanization of intuitionistic multiplicative-additive linear logic. In: Types for Proofs and Programs, TYPES. LIPIcs, vol. 104, pp. 1:1\u20131:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2017.1","DOI":"10.4230\/LIPIcs.TYPES.2017.1"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Atkey, R.: Syntax and semantics of quantitative type theory. In: Logic in Computer Science, LICS, pp. 56\u201365. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209189","DOI":"10.1145\/3209108.3209189"},{"issue":"6","key":"9_CR4","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1017\/S0960129500070109","volume":"6","author":"E Barendsen","year":"1996","unstructured":"Barendsen, E., Smetsers, S.: Uniqueness typing for functional languages with graph rewriting semantics. Math. Struct. Comput. Sci. 6(6), 579\u2013612 (1996)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9_CR5","unstructured":"Bengtson, J.: The pi-calculus in nominal logic, vol. 2012 (2012). https:\/\/www.isa-afp.org\/entries\/Pi_Calculus.shtml"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-030-45237-7_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Castro","year":"2020","unstructured":"Castro, D., Ferreira, F., Yoshida, N.: EMTST: engineering the meta-theory of session types. TACAS 2020. LNCS, vol. 12079, pp. 278\u2013285. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_17"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Cervesato, I., Pfenning, F.: A linear logical framework. In: Logic in Computer Science, LICS, pp. 264\u2013275. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561339","DOI":"10.1109\/LICS.1996.561339"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Ciccone, L., Padovani, L.: A dependently typed linear $$\\pi $$-calculus in Agda. In: PPDP 2020: 22nd International Symposium on Principles and Practice of Declarative Programming, pp. 8:1\u20138:14. ACM (2020). https:\/\/doi.org\/10.1145\/3414080.3414109","DOI":"10.1145\/3414080.3414109"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Dardha, O.: Recursive session types revisited. In: Carbone, M. (ed.) Workshop on Behavioural Types, BEAT. EPTCS, vol. 162, pp. 27\u201334 (2014). https:\/\/doi.org\/10.4204\/EPTCS.162.4","DOI":"10.4204\/EPTCS.162.4"},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.ic.2017.06.002","volume":"256","author":"O Dardha","year":"2017","unstructured":"Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. Inf. Comput. 256, 253\u2013286 (2017). https:\/\/doi.org\/10.1016\/j.ic.2017.06.002. Extended version of [10]","journal-title":"Inf. Comput."},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In: Indagationes Mathematicae (Proceedings), vol. 75, pp. 381\u2013392. Elsevier (1972)","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"9_CR12","unstructured":"Deransart, P., Smaus, J.: Subject reduction of logic programs as proof-theoretic property, vol. 2002 (2002). http:\/\/danae.uni-muenster.de\/lehre\/kuchen\/JFLP\/articles\/2002\/S02-01\/JFLP-A02-02.pdf"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/3-540-44929-9_30","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"J Despeyroux","year":"2000","unstructured":"Despeyroux, J.: A higher-order specification of the $$\\pi $$-Calculus. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.) TCS 2000. LNCS, vol. 1872, pp. 425\u2013439. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44929-9_30"},{"issue":"4","key":"9_CR14","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P Dybjer","year":"1994","unstructured":"Dybjer, P.: Inductive families. Formal Asp. Comput. 6(4), 440\u2013465 (1994). https:\/\/doi.org\/10.1007\/BF01211308","journal-title":"Formal Asp. Comput."},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-44755-5_16","volume-title":"Theorem Proving in Higher Order Logics","author":"SJ Gay","year":"2001","unstructured":"Gay, S.J.: A framework for the formalisation of pi calculus type systems in Isabelle\/HOL. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 217\u2013232. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44755-5_16"},{"issue":"1","key":"9_CR16","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1017\/S0956796809990268","volume":"20","author":"SJ Gay","year":"2010","unstructured":"Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19\u201350 (2010). https:\/\/doi.org\/10.1017\/S0956796809990268","journal-title":"J. Funct. Program."},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-662-54434-1_20","volume-title":"Programming Languages and Systems","author":"AL Georges","year":"2017","unstructured":"Georges, A.L., Murawska, A., Otis, S., Pientka, B.: LINCX: a linear logical framework with first-class contexts. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 530\u2013555. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_20"},{"issue":"3","key":"9_CR18","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1017\/S0960129514000231","volume":"26","author":"MA Goto","year":"2016","unstructured":"Goto, M.A., Jagadeesan, R., Jeffrey, A., Pitcher, C., Riely, J.: An extensible approach to session polymorphism. Math. Struct. Comput. Sci. 26(3), 465\u2013509 (2016). https:\/\/doi.org\/10.1017\/S0960129514000231","journal-title":"Math. Struct. Comput. Sci."},{"issue":"2","key":"9_CR19","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"253","author":"F Honsell","year":"2001","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: pi-calculus in (Co)inductive-type theory. Theor. Comput. Sci. 253(2), 239\u2013285 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(00)00095-5","journal-title":"Theor. Comput. Sci."},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Jung, R., et al.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: Rajamani, S.K., Walker, D. (eds.) Symposium on Principles of Programming Languages, POPL 2015, pp. 637\u2013650. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"9_CR21","unstructured":"Kobayashi, N.: Type systems for concurrent programs (2007). http:\/\/www.kb.ecei.tohoku.ac.jp\/~koba\/papers\/tutorial-type-extended.pdf"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the Pi-Calculus. In: Symposium on Principles of Programming Languages, POPL, pp. 358\u2013371. ACM Press (1996). https:\/\/doi.org\/10.1145\/237721.237804","DOI":"10.1145\/237721.237804"},{"issue":"4","key":"9_CR23","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1017\/S0956796800001131","volume":"4","author":"I Mackie","year":"1994","unstructured":"Mackie, I.: Lilac: a functional programming language based on linear logic. J. Funct. Program. 4(4), 395\u2013433 (1994). https:\/\/doi.org\/10.1017\/S0956796800001131","journal-title":"J. Funct. Program."},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Matsakis, N.D., II, F.S.K.: The rust language. In: High Integrity Language Technology, HILT, pp. 103\u2013104. ACM (2014). https:\/\/doi.org\/10.1145\/2663171.2663188","DOI":"10.1145\/2663171.2663188"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-319-30936-1_12","volume-title":"A List of Successes That Can Change the World","author":"C McBride","year":"2016","unstructured":"McBride, C.: I got plenty o\u2019 Nuttin\u2019. In: Lindley, S., McBride, C., Trinder, P., Sannella, D. (eds.) A List of Successes That Can Change the World. LNCS, vol. 9600, pp. 207\u2013233. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30936-1_12"},{"key":"9_CR26","volume-title":"Communicating and Mobile Systems - The Pi-calculus","author":"R Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems - The Pi-calculus. Cambridge University Press, Cambridge (1999)"},{"issue":"1","key":"9_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Parts I and II. Inf. Comput. 100(1), 1\u201340 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90008-4","journal-title":"Inf. Comput."},{"key":"9_CR28","doi-asserted-by":"publisher","unstructured":"Orchard, D., Liepelt, V., III, H.E.: Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang. 3(ICFP), 110:1\u2013110:30 (2019). https:\/\/doi.org\/10.1145\/3341714","DOI":"10.1145\/3341714"},{"key":"9_CR29","doi-asserted-by":"publisher","unstructured":"Orchard, D.A., Yoshida, N.: Using session types as an effect system. In: Gay, S., Alglave, J. (eds.) Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES 2015. EPTCS, vol. 203, pp. 1\u201313 (2015). https:\/\/doi.org\/10.4204\/EPTCS.203.1","DOI":"10.4204\/EPTCS.203.1"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Rouvoet, A., Poulsen, C.B., Krebbers, R., Visser, E.: Intrinsically-typed definitional interpreters for linear, session-typed languages. In: Certified Programs and Proofs, CPP, pp. 284\u2013298. ACM (2020). https:\/\/doi.org\/10.1145\/3372885.3373818","DOI":"10.1145\/3372885.3373818"},{"key":"9_CR31","doi-asserted-by":"crossref","DOI":"10.1017\/9781316134924","volume-title":"The Pi-Calculus - A Theory of Mobile Processes","author":"D Sangiorgi","year":"2001","unstructured":"Sangiorgi, D., Walker, D.: The Pi-Calculus - A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A linear decomposition of multiparty sessions for safe distributed programming. In: European Conference on Object-Oriented Programming, ECOOP. LIPIcs, vol. 74, pp. 24:1\u201324:31. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2017.24","DOI":"10.4230\/LIPIcs.ECOOP.2017.24"},{"key":"9_CR33","doi-asserted-by":"publisher","unstructured":"Thiemann, P.: Intrinsically-typed mechanized semantics for session types, pp. 19:1\u201319:15 (2019). https:\/\/doi.org\/10.1145\/3354166.3354184","DOI":"10.1145\/3354166.3354184"},{"key":"9_CR34","doi-asserted-by":"publisher","unstructured":"Turon, A.J., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical relations for fine-grained concurrency. In: Giacobazzi, R., Cousot, R. (eds.) Symposium on Principles of Programming Languages, POPL 2013, pp. 343\u2013356. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429111","DOI":"10.1145\/2429069.2429111"},{"key":"9_CR35","unstructured":"Wadler, P.: Linear types can change the world! In: Programming Concepts and Methods, p. 561. North-Holland (1990)"},{"key":"9_CR36","unstructured":"Zalakain, U., Dardha, O.: $$\\pi $$ with leftovers: a mechanisation in Agda. CoRR abs\/2005.05902 (2020). https:\/\/arxiv.org\/abs\/2005.05902"},{"key":"9_CR37","unstructured":"Zalakain, U., Dardha, O.: Typing the linear $$\\pi $$-Calculus \u2013 formalisation in Agda (2021). https:\/\/github.com\/umazalakain\/typing-linear-pi"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-78089-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,8]],"date-time":"2025-06-08T22:04:07Z","timestamp":1749420247000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-78089-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030780883","9783030780890"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-78089-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"8 June 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Techniques for Distributed Objects, Components, and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Valletta","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Malta","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 June 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 June 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"41","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"forte2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2021\/forte","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":"26","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":"9","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":"4","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":"35% - 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":"2","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":"Due to the Corona pandemic this event was held virtually.","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)"}}]}}