{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,3]],"date-time":"2025-10-03T18:17:29Z","timestamp":1759515449671},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,9,14]],"date-time":"2020-09-14T00:00:00Z","timestamp":1600041600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,9,14]],"date-time":"2020-09-14T00:00:00Z","timestamp":1600041600000},"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":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,1]]},"DOI":"10.1007\/s10817-020-09553-0","type":"journal-article","created":{"date-parts":[[2020,9,14]],"date-time":"2020-09-14T14:02:47Z","timestamp":1600092167000},"page":"75-124","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["HO$$\\pi $$ in Coq"],"prefix":"10.1007","volume":"65","author":[{"given":"Guillaume","family":"Ambal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergue\u00ef","family":"Lenglet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Schmitt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,9,14]]},"reference":[{"key":"9553_CR1","first-page":"221","volume-title":"TPHOLs\u201999, Volume 1690 of Lecture Notes in Computer Science","author":"S Ambler","year":"1999","unstructured":"Ambler, S., Crole, R.L.: Mechanized operational semantics via (co)induction. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin-Mohring, C., Th\u00e9ry, L. (eds.) TPHOLs\u201999, Volume 1690 of Lecture Notes in Computer Science, pp. 221\u2013238. Springer, Nice (1999)"},{"key":"9553_CR2","first-page":"27","volume-title":"ITP 2014, Volume 8558 of Lecture Notes in Computer Science","author":"A Anand","year":"2014","unstructured":"Anand, A., Rahli, V.: Towards a formally verified proof assistant. In: Klein, G., Gamboa, R. (eds.) ITP 2014, Volume 8558 of Lecture Notes in Computer Science, pp. 27\u201344. Springer, Vienna (2014)"},{"key":"9553_CR3","doi-asserted-by":"crossref","unstructured":"Aydemir, B., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: the PoplMark challenge. In: TPHOLs, pp. 50\u201365 (2005)","DOI":"10.1007\/11541868_4"},{"key":"9553_CR4","unstructured":"Aydemir, B.E., Weirich, S.: LNgen: tool support for locally nameless representations. Technical report, University of Pennsylvania (2010)"},{"issue":"2","key":"9553_CR5","first-page":"1","volume":"7","author":"D Baelde","year":"2014","unstructured":"Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: a system for reasoning about relational specifications. J. Formaliz. Reason. 7(2), 1\u201389 (2014)","journal-title":"J. Formaliz. Reason."},{"issue":"2","key":"9553_CR6","doi-asserted-by":"publisher","first-page":"16","DOI":"10.2168\/LMCS-5(2:16)2009","volume":"5","author":"J Bengtson","year":"2009","unstructured":"Bengtson, J., Parrow, J.: Formalising the pi-calculus using nominal logic. Log. Methods Comput. Sci. 5(2), 16 (2009)","journal-title":"Log. Methods Comput. Sci."},{"issue":"1","key":"9553_CR7","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1017\/S0956796899003366","volume":"9","author":"RS Bird","year":"1999","unstructured":"Bird, R.S., Paterson, R.: De Bruijn notation as a nested datatype. J. Funct. Program. 9(1), 77\u201391 (1999)","journal-title":"J. Funct. Program."},{"issue":"3","key":"9553_CR8","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1017\/S0956796806005892","volume":"16","author":"A Bucalo","year":"2006","unstructured":"Bucalo, A., Honsell, F., Miculan, M., Scagnetto, I., Hofmann, M.: Consistency of the theory of contexts. J. Funct. Program. 16(3), 327\u2013372 (2006)","journal-title":"J. Funct. Program."},{"issue":"1","key":"9553_CR9","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1006\/inco.2001.2951","volume":"179","author":"I Cervesato","year":"2002","unstructured":"Cervesato, I., Pfenning, F.: A linear logical framework. Inf. Comput. 179(1), 19\u201375 (2002)","journal-title":"Inf. Comput."},{"key":"9553_CR10","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Pfenning, F., Walker, D., Watkins, K.: A concurrent logical framework II: examples and applications. Technical report CMU-CS-02-102, Carnegie Mellon University (2002)","DOI":"10.21236\/ADA418538"},{"key":"9553_CR11","unstructured":"Chargu\u00e9raud, A.: LN: locally nameless representation with cofinite quantification. http:\/\/www.chargueraud.org\/softs\/ln\/"},{"key":"9553_CR12","unstructured":"Chargu\u00e9raud, A.: TLC: a non-constructive library for Coq. http:\/\/www.chargueraud.org\/softs\/tlc\/"},{"issue":"3","key":"9553_CR13","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","volume":"49","author":"A Chargu\u00e9raud","year":"2012","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. J. Autom. Reason. 49(3), 363\u2013408 (2012)","journal-title":"J. Autom. Reason."},{"key":"9553_CR14","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.tcs.2015.07.019","volume":"606","author":"A Ciaffaglione","year":"2015","unstructured":"Ciaffaglione, A., Scagnetto, I.: Mechanizing type environments in weak HOAS. Theor. Comput. Sci. 606, 57\u201378 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"9553_CR15","doi-asserted-by":"crossref","unstructured":"Dal Zilio, S.: Mobile processes: a commented bibliography. In: MOVEP\u20192K\u20144th Summer school on Modelling and Verification of Parallel Processes, Volume 2067 of Lecture Notes in Computer Science, pp. 206\u2013222. Springer (2001)","DOI":"10.1007\/3-540-45510-8_11"},{"issue":"5","key":"9553_CR16","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"NG de Bruijn","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies: a tool for automatic formula manipulation, with application to the Church\u2013Rosser theorem. Indag. Math. 75(5), 381\u2013392 (1972)","journal-title":"Indag. Math."},{"key":"9553_CR17","first-page":"425","volume-title":"IFIP TCS 2000, Volume 1872 of Lecture Notes in Computer Science","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.) IFIP TCS 2000, Volume 1872 of Lecture Notes in Computer Science, pp. 425\u2013439. Springer, New York (2000)"},{"key":"9553_CR18","first-page":"124","volume-title":"TLCA \u201d95, Volume 902 of Lecture Notes in Computer Science","author":"J Despeyroux","year":"1995","unstructured":"Despeyroux, J., Felty, A.P., Hirschowitz, A.: Higher-order abstract syntax in coq. In: Dezani-Ciancaglini, M., Plotkin, G.D. (eds.) TLCA \u201d95, Volume 902 of Lecture Notes in Computer Science, pp. 124\u2013138. Springer, New York (1995)"},{"key":"9553_CR19","first-page":"217","volume-title":"TPHOLs 2001","author":"SJ Gay","year":"2001","unstructured":"Gay, S.J.: A framework for the formalisation of pi calculus type systems in Isabelle\/HOL. In: Boulton, Richard J., Jackson, Paul B. (eds.) TPHOLs 2001, vol. 2152, pp. 217\u2013232. Springer, Edinburgh (2001)"},{"key":"9553_CR20","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1016\/S1571-0661(04)80013-6","volume":"1","author":"AD Gordon","year":"1995","unstructured":"Gordon, A.D.: Bisimilarity as a theory of functional programming. Electron. Notes Theor. Comput. Sci. 1, 232\u2013252 (1995)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9553_CR21","unstructured":"Henry-Gr\u00e9ard, L.: Proof of the subject reduction property for a pi-calculus in COQ. Technical report RR-3698, INRIA (1999)"},{"key":"9553_CR22","doi-asserted-by":"crossref","unstructured":"Hirschkoff, D.: A full formalisation of pi-calculus theory in the calculus of constructions. In: Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, vol. 1275, pp. 153\u2013169. Springer (1997)","DOI":"10.1007\/BFb0028392"},{"key":"9553_CR23","unstructured":"Hirschkoff, D.: Up to context proofs for the $$\\pi $$-calculus in the Coq system. Technical report 97-82, CERMICS (1997)"},{"key":"9553_CR24","doi-asserted-by":"crossref","unstructured":"Hirschkoff, D., Pous, D.: A distribution law for CCS and a new congruence result for the pi-calculus. In: Proceedings of FoSSaCS\u201907, Volume 4423 of LNCS, pp. 228\u2013242. Springer (2007)","DOI":"10.1007\/978-3-540-71389-0_17"},{"issue":"2","key":"9553_CR25","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"253","author":"F Honsell","year":"2000","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: pi-calculus in (co)inductive-type theory. Theor. Comput. Sci. 253(2), 239\u2013285 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"9553_CR26","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1016\/S1571-0661(04)00323-8","volume":"62","author":"F Honsell","year":"2001","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: The theory of contexts for first order and higher order abstract syntax. Electr. Notes Theor. Comput. Sci. 62, 116\u2013135 (2001)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"2","key":"9553_CR27","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1006\/inco.1996.0008","volume":"124","author":"DJ Howe","year":"1996","unstructured":"Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Inf. Comput. 124(2), 103\u2013112 (1996)","journal-title":"Inf. Comput."},{"key":"9553_CR28","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-94-017-0253-9_10","volume":"28","author":"MJ Gabbay","year":"2003","unstructured":"Gabbay, M.J.: The pi-calculus in FM. Thirty Five Years Autom. Math. 28, 247\u2013269 (2003)","journal-title":"Thirty Five Years Autom. Math."},{"key":"9553_CR29","doi-asserted-by":"crossref","unstructured":"Keuchel, S., Weirich, S., Schrijvers, T.: Needle & knot: binder boilerplate tied up. In: ESOP 16, Volume 9632 of Lecture Notes in Computer Science, pp. 419\u2013445. Springer (2016)","DOI":"10.1007\/978-3-662-49498-1_17"},{"key":"9553_CR30","unstructured":"Lenglet, S., Schmitt, A.: Howe\u2019s method for contextual semantics. In: Aceto, L., de Frutos-Escrig, D. (eds.) 26th International Conference on Concurrency Theory, CONCUR 2015, Volume 42 of LIPIcs, pp. 212\u2013225. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Madrid, Spain (2015)"},{"key":"9553_CR31","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1145\/3167083","volume-title":"CPP 2018","author":"S Lenglet","year":"2018","unstructured":"Lenglet, S., Schmitt, A.: HO$$\\pi $$ in Coq. In: Andronick, J., Felty, A.P. (eds.) CPP 2018, pp. 252\u2013265. ACM, Copenhagen (2018)"},{"issue":"11","key":"9553_CR32","doi-asserted-by":"publisher","first-page":"1390","DOI":"10.1016\/j.ic.2011.08.002","volume":"209","author":"S Lenglet","year":"2011","unstructured":"Lenglet, S., Schmitt, A., Stefani, J.-B.: Characterizing contextual equivalence in calculi with passivation. Inf. Comput. 209(11), 1390\u20131433 (2011)","journal-title":"Inf. Comput."},{"key":"9553_CR33","first-page":"278","volume-title":"ITP 2015, Volume 9236 of Lecture Notes in Computer Science","author":"P Maksimovic","year":"2015","unstructured":"Maksimovic, P., Schmitt, A.: Hocore in Coq. In: Urban, C., Zhang, X. (eds.) ITP 2015, Volume 9236 of Lecture Notes in Computer Science, pp. 278\u2013293. Springer, Nanjing (2015)"},{"key":"9553_CR34","first-page":"289","volume-title":"TLCA \u201993, Volume 664 of Lecture Notes in Computer Science","author":"J McKinna","year":"1993","unstructured":"McKinna, J., Pollack, R.: Pure type systems formalized. In: Bezem, M., Groote, J.F. (eds.) TLCA \u201993, Volume 664 of Lecture Notes in Computer Science, pp. 289\u2013305. Springer, New York (1993)"},{"issue":"1","key":"9553_CR35","first-page":"50","volume":"1","author":"TF Melham","year":"1994","unstructured":"Melham, T.F.: A mechanized theory of the pi-calculus in HOL. Nord. J. Comput. 1(1), 50\u201376 (1994)","journal-title":"Nord. J. Comput."},{"issue":"4","key":"9553_CR36","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/1094622.1094628","volume":"6","author":"D Miller","year":"2005","unstructured":"Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Log. 6(4), 749\u2013783 (2005)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1","key":"9553_CR37","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. I. Inf. Comput. 100(1), 1\u201340 (1992)","journal-title":"Inf. Comput."},{"key":"9553_CR38","doi-asserted-by":"crossref","unstructured":"Mohamed, O.A.: Mechanizing a pi-calculus equivalence in hol. In: TPHOL 95, pp. 1\u201316. Springer (1995)","DOI":"10.1007\/3-540-60275-5_53"},{"key":"9553_CR39","doi-asserted-by":"crossref","unstructured":"Momigliano, A.: A supposedly fun thing I may have to do again: a HOAS encoding of Howe\u2019s method. In: LFMTP 12, pp. 33\u201342(2012). ACM, Copenhagen, Denmark","DOI":"10.1145\/2364406.2364411"},{"key":"9553_CR40","first-page":"1","volume":"First View","author":"J Parrow","year":"2014","unstructured":"Parrow, J., Borgstr\u00f6m, J., Raabjerg, P., \u00c5man Pohjola, J.: Higher-order psi-calculi. Math. Struct. Comput. Sci. First View, 1\u201337 (2014)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"9","key":"9553_CR41","doi-asserted-by":"crossref","first-page":"1541","DOI":"10.1017\/S096012951700010X","volume":"28","author":"R Perera","year":"2018","unstructured":"Perera, R., Cheney, J.: Proof-relevant $$\\pi $$-calculus: a constructive account of concurrency and causality. Math. Struct. Comput. Sci. 28(9), 1541\u20131577 (2018)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9553_CR42","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: PLDI 88, pp. 199\u2013208. ACM, Atlanta, Georgia, USA (1988)","DOI":"10.1145\/960116.54010"},{"key":"9553_CR43","first-page":"202","volume-title":"CADE 99, Volume 1632 of Lecture Notes in Computer Science","author":"F Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf\u2014a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 99, Volume 1632 of Lecture Notes in Computer Science, pp. 202\u2013206. Springer, New York (1999)"},{"key":"9553_CR44","first-page":"15","volume-title":"IJCAR 2010, Volume of 6173 Lecture Notes in Computer Science","author":"B Pientka","year":"2010","unstructured":"Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (system description). In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010, Volume of 6173 Lecture Notes in Computer Science, pp. 15\u201321. Springer, Edinburgh (2010)"},{"issue":"2","key":"9553_CR45","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"AM Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165\u2013193 (2003)","journal-title":"Inf. Comput."},{"issue":"1","key":"9553_CR46","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S1571-0661(04)00276-2","volume":"58","author":"C R\u00f6ckl","year":"2001","unstructured":"R\u00f6ckl, C.: A first-order syntax for the pi-calculus in isabelle\/hol using permutations. Electr. Notes Theor. Comput. Sci. 58(1), 1\u201317 (2001)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"2","key":"9553_CR47","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1017\/S0956796802004653","volume":"13","author":"C R\u00f6ckl","year":"2003","unstructured":"R\u00f6ckl, C., Hirschkoff, D.: A fully adequate shallow embedding of the [pi]-calculus in isabelle\/hol with mechanized syntax analysis. J. Funct. Program. 13(2), 415\u2013451 (2003)","journal-title":"J. Funct. Program."},{"issue":"2","key":"9553_CR48","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1006\/inco.1996.0096","volume":"131","author":"D Sangiorgi","year":"1996","unstructured":"Sangiorgi, D.: Bisimulation for higher-order process calculi. Inf. Comput. 131(2), 141\u2013178 (1996)","journal-title":"Inf. Comput."},{"key":"9553_CR49","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":"9553_CR50","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1145\/3293880.3294101","volume-title":"CPP 19","author":"K Stark","year":"2019","unstructured":"Stark, K., Sch\u00e4fer, S., Kaiser, J.: Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. In: Mahboubi, A., Myreen, M.O. (eds.) CPP 19, pp. 166\u2013180. ACM, Copenhagen (2019)"},{"key":"9553_CR51","unstructured":"The Penn PL Club: The Penn locally nameless metatheory library. https:\/\/github.com\/plclub\/metalib"},{"key":"9553_CR52","unstructured":"Thibodeau, D., Momigliano, A., Pientka, B.: A case-study in programming coinductive proofs: Howe\u2019s method. http:\/\/www.momigliano.di.unimi.it\/papers\/bhowe.pdf (2016)"},{"issue":"4","key":"9553_CR53","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","volume":"40","author":"C Urban","year":"2008","unstructured":"Urban, C.: Nominal techniques in Isabelle\/HOL. J. Autom. Reason. 40(4), 327\u2013356 (2008)","journal-title":"J. Autom. Reason."},{"key":"9553_CR54","unstructured":"Urban, C., Berghofer, S., Kaliszyk, C.: Nominal 2. Archive of Formal Proofs (2013). http:\/\/isa-afp.org\/entries\/Nominal2.html, Formal proof development"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09553-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09553-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09553-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,7]],"date-time":"2023-10-07T08:45:29Z","timestamp":1696668329000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09553-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,14]]},"references-count":54,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1]]}},"alternative-id":["9553"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09553-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,9,14]]},"assertion":[{"value":"19 December 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 April 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 September 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}