{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T21:22:38Z","timestamp":1784150558371,"version":"3.55.0"},"reference-count":64,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2018,10,31]],"date-time":"2018-10-31T00:00:00Z","timestamp":1540944000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2019,9]]},"abstract":"<jats:p>Bisimulation proofs play a central role in programming languages in establishing rich properties such as contextual equivalence. They are also challenging to mechanize, since they require a combination of inductive and coinductive reasoning on open terms. In this paper, we describe mechanizing the property that similarity in the call-by-name lambda calculus is a pre-congruence using Howe\u2019s method in the<jats:monospace>Beluga<\/jats:monospace>formal reasoning system. The development relies on three key ingredients: (1) we give a higher order abstract syntax (HOAS) encoding of lambda terms together with their operational semantics as intrinsically typed terms, thereby avoiding not only the need to deal with binders, renaming and substitutions, but keeping all typing invariants implicit; (2) we take advantage of<jats:monospace>Beluga<\/jats:monospace>\u2019s support for representing open terms using built-in contexts and simultaneous substitutions: this allows us to directly state central definitions such as open simulation without resorting to the usual inductive closure operation and to encode very elegantly notoriously painful proofs such as the substitutivity of the Howe relation; (3) we exploit the possibility of reasoning by coinduction in<jats:monospace>Beluga<\/jats:monospace>\u2019s reasoning logic. The end result is succinct and elegant, thanks to the high-level abstractions and primitives<jats:monospace>Beluga<\/jats:monospace>provides. We believe that this mechanization is a significant example that illustrates<jats:monospace>Beluga<\/jats:monospace>\u2019s strength at mechanizing challenging (co)inductive proofs using HOAS encodings.<\/jats:p>","DOI":"10.1017\/s0960129518000415","type":"journal-article","created":{"date-parts":[[2018,10,31]],"date-time":"2018-10-31T10:47:55Z","timestamp":1540982875000},"page":"1309-1343","source":"Crossref","is-referenced-by-count":6,"title":["A case study in programming coinductive proofs: Howe\u2019s method"],"prefix":"10.1017","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0942-4777","authenticated-orcid":false,"given":"ALBERTO","family":"MOMIGLIANO","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"BRIGITTE","family":"PIENTKA","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"DAVID","family":"THIBODEAU","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2018,10,31]]},"reference":[{"key":"S0960129518000415_ref37","first-page":"434","volume-title":"Proceedings of the 12th Symposium on Logic in Computer Science","author":"McDowell","year":"1997"},{"key":"S0960129518000415_ref20","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1145\/2676724.2693170","volume-title":"Proceedings of the 2015 Conference on Certified Programs and Proofs (CPP 2015)","author":"Chaudhuri","year":"2015"},{"key":"S0960129518000415_ref64","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2012.07.007"},{"key":"S0960129518000415_ref21","first-page":"311","article-title":"\u03b1check: A mechanized metatheory model checker","volume":"17","author":"Cheney","year":"2017","journal-title":"TPLP"},{"key":"S0960129518000415_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.010"},{"key":"S0960129518000415_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_15"},{"key":"S0960129518000415_ref7","first-page":"195","volume-title":"Proceedings of the 6th Conference on Certified Programs and Proofs (CPP'17)","author":"Allais","year":"2017"},{"key":"S0960129518000415_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_14"},{"key":"S0960129518000415_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429075"},{"key":"S0960129518000415_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/2364406.2364411"},{"key":"S0960129518000415_ref17","first-page":"18","volume-title":"Proceedings of the 10th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'15)","author":"Cave","year":"2015"},{"key":"S0960129518000415_ref1","unstructured":"Abel A. (2012). Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. In: Proceedings of the Invited Talk at 8th Workshop on Fixed-points in Computer Science (FICS'12) 1\u201311."},{"key":"S0960129518000415_ref5","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1991.9999"},{"key":"S0960129518000415_ref16","first-page":"15","volume-title":"Proceedings of the 8th ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'13)","author":"Cave","year":"2013"},{"key":"S0960129518000415_ref34","unstructured":"Lee D. K. , Crary K. and Harper R. (2007). Towards a mechanized metatheory of Standard ML. In: Proceedings of the 34th Symposium on Principles of Programming Languages (POPL'07), ACM Press, 173\u2013184."},{"key":"S0960129518000415_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9194-x"},{"key":"S0960129518000415_ref24","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025689206562"},{"key":"S0960129518000415_ref53","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"S0960129518000415_ref31","unstructured":"Jacob-Rao R. , Pientka B. and Thibodeau D. (2018). Index-stratified types. In: Kirchner H. (ed.) Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD'18), LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 19:1\u201319:17."},{"key":"S0960129518000415_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000154"},{"key":"S0960129518000415_ref15","first-page":"413","volume-title":"Proceedings of the 39th Symposium on Principles of Programming Languages (POPL'12)","author":"Cave","year":"2012"},{"key":"S0960129518000415_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000022"},{"key":"S0960129518000415_ref9","first-page":"1","article-title":"Abella: A system for reasoning about relational specifications","volume":"7","author":"Baelde","year":"2014","journal-title":"Journal of Formalized Reasoning"},{"key":"S0960129518000415_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028392"},{"key":"S0960129518000415_ref45","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80506-1"},{"key":"S0960129518000415_ref35","unstructured":"Lenglet S. and Schmitt A. (2018). Ho\u03c0 in coq. In: Andronick J. and Felty A.P. (eds.) Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), Los Angeles, CA, USA, January 8\u20139, 2018, ACM, 252\u2013265."},{"key":"S0960129518000415_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00095-5"},{"key":"S0960129518000415_ref36","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000125"},{"key":"S0960129518000415_ref2","unstructured":"Abel A. and Pientka B. (2013). Well-founded recursion with copatterns: A unified approach to termination and productivity. In: Proceedings of the 18th International Conference on Functional Programming (ICFP'13) 185\u2013196."},{"key":"S0960129518000415_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/3167093"},{"key":"S0960129518000415_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"key":"S0960129518000415_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"S0960129518000415_ref61","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588.006"},{"key":"S0960129518000415_ref40","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326"},{"key":"S0960129518000415_ref25","first-page":"103","volume-title":"Proceedings of the 27th International Colloquium, Automata, Languages and Programming (ICALP 2000)","author":"Ghica","year":"2000"},{"key":"S0960129518000415_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"S0960129518000415_ref6","first-page":"69","volume-title":"Proceedings of the 15th European Symposium on Programming (ESOP'06)","author":"Ahmed","year":"2006"},{"key":"S0960129518000415_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"S0960129518000415_ref59","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.007"},{"key":"S0960129518000415_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_28"},{"key":"S0960129518000415_ref14","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-319-66167-4_1","volume-title":"Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS'17)","author":"Biendarra","year":"2017"},{"key":"S0960129518000415_ref26","unstructured":"Gim\u00e9nez E. (1996). Un Calcul de Constructions Infinies et son application \u00e0 la v\u00e9rification de syst\u00e8mes communicants. PhD thesis, Ecole Normale Sup\u00e9rieure de Lyon, Th\u00e8se d'universit\u00e9."},{"key":"S0960129518000415_ref48","unstructured":"Oury N. (2008). Coinductive types and type preservation. Message on the coq-club mailing list."},{"key":"S0960129518000415_ref11","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(2:16)2009"},{"key":"S0960129518000415_ref57","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389469"},{"key":"S0960129518000415_ref52","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-6534-3"},{"key":"S0960129518000415_ref47","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"S0960129518000415_ref49","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000170"},{"key":"S0960129518000415_ref56","unstructured":"Pientka B. and Cave A. (2015). Inductive Beluga: Programming proofs (system description). In: Felty A.P. and Middeldorp A. (eds.) Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Computer Science, vol. 9195, Springer, 272\u2013281."},{"key":"S0960129518000415_ref50","unstructured":"Pfenning F. (1997). Computation and deduction. Accessed January 31st, 2018."},{"key":"S0960129518000415_ref62","first-page":"351","volume-title":"Proceedings of the 21st International Conference on Functional Programming (ICFP'16)","author":"Thibodeau","year":"2016"},{"key":"S0960129518000415_ref54","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000408"},{"key":"S0960129518000415_ref55","unstructured":"Pientka B. and Abel A. (2015). Structural recursion over contextual objects. In Altenkirch T. (ed.) Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15), Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl, 273\u2013287."},{"key":"S0960129518000415_ref60","first-page":"245","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pitts","year":"2005"},{"key":"S0960129518000415_ref63","doi-asserted-by":"publisher","DOI":"10.1145\/1656242.1656248"},{"key":"S0960129518000415_ref30","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"S0960129518000415_ref39","unstructured":"McLaughlin C. , McKinna J. and Stark I. (2018). Triangulating context lemmas. In: Andronick J. and Felty A.P. (eds.) Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), Los Angeles, CA, USA, January 8\u20139, 2018, ACM, 102\u2013114."},{"key":"S0960129518000415_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/333580.333590"},{"key":"S0960129518000415_ref33","unstructured":"Lassen S. B. (1998). Relational Reasoning About Functions and Nondeterminism. PhD thesis, Department of Computer Science, University of Aarhus."},{"key":"S0960129518000415_ref58","doi-asserted-by":"crossref","unstructured":"Pientka B. and Dunfield J. (2010). Beluga: A framework for programming and reasoning with deductive systems (System Description). In: Giesl J. and Haehnle R. (eds.) Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR'10), Lecture Notes in Artificial Intelligence, vol. 6173, Springer, 15\u201321.","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"S0960129518000415_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80412-8"},{"key":"S0960129518000415_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9336-2"},{"key":"S0960129518000415_ref46","unstructured":"Momigliano A. and Tiu A. (2003). Induction and co-induction in sequent calculus. In: Coppo M. , Berardi S. and Damiani F. (eds.) Post-Proceedings of TYPES 2003, Lecture Notes in Computer Science, vol. 3085, 293\u2013308."},{"key":"S0960129518000415_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/3131851.3131869"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129518000415","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,4]],"date-time":"2022-09-04T23:50:18Z","timestamp":1662335418000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129518000415\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,31]]},"references-count":64,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["S0960129518000415"],"URL":"https:\/\/doi.org\/10.1017\/s0960129518000415","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,10,31]]}}}