{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:11:50Z","timestamp":1761610310561,"version":"build-2065373602"},"reference-count":25,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3893,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,12]]},"DOI":"10.1016\/s1571-0661(04)80506-1","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"60-75","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":10,"title":["A Hybrid Encoding of Howe's Method for Establishing Congruence of Bisimilarity"],"prefix":"10.1016","volume":"70","author":[{"given":"Alberto","family":"Momigliano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon J.","family":"Ambler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roy L.","family":"Crole","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB1","doi-asserted-by":"crossref","unstructured":"A. Gordon. A mechanisation of name-carrying syntax up to alpha-conversion. In J.J. Joyce and C.-J.H. Seger, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, volume 780 of Lecture Notes in Computer Science, pages 414\u2013427, Vancouver, Canada, Aug. 1993. University of British Columbia, Springer-Verlag, published 1994.","DOI":"10.1007\/3-540-57826-9_152"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB2","series-title":"Research Topics in Functional Programming","first-page":"65","article-title":"The lazy lambda calculus","author":"Abramsky","year":"1990"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB3","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1006\/inco.1993.1044","article-title":"Full abstraction in the lazy lambda calculus","volume":"105","author":"Abramsky","year":"1992","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB4","unstructured":"S. Ambler, R. Crole, and A. Momigliano. Combining higher order abstract syntax with tactical theorem proving and (co)induction. In In V. A. Carre\u00f1o editor Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, Hampton, VA, 1\u20133 August 2002, pages 327\u2013343, volume 2342 Lecture Notes in Computer Science, Springer Verlag, Berlin, 2002."},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB5","doi-asserted-by":"crossref","unstructured":"S. J. Ambler and R. L. Crole. Mechanised Operational Semantics via (Co)Induction. In Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, volume 1690 of Lecture Notes in Computer Science, pages 221\u2013238. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48256-3_15"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB6","doi-asserted-by":"crossref","unstructured":"N. Benton and A. Kennedy. Monads, effects and transformations. In Proceedings of the 3rd International Workshop in Higher Order Operational Techniques in Semantics, volume 26 of Electronic Notes in Theoretical Computer Science. Elsevier, 1998.","DOI":"10.1016\/S1571-0661(05)80280-4"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB7","doi-asserted-by":"crossref","unstructured":"I. Cervesato and F. Pfenning. A linear logical framework. In E. Clarke, editor, Proceedings of the Eleventh Annual Symposium on Logic in Computer Science, pages 264\u2013275, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1996.561339"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB8","doi-asserted-by":"crossref","unstructured":"J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-order abstract syntax in Coq. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 124\u2013138, Edinburgh, Scotland, Apr. 1995. Springer-Verlag LNCS 902.","DOI":"10.1007\/BFb0014049"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB9","doi-asserted-by":"crossref","unstructured":"L.-H. Eriksson. Pi: An interactive derivation editor for the calculus of partial inductive definitions. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, pages 821\u2013825, Nancy, France, June 1994. Springer Verlag LNAI 814.","DOI":"10.1007\/3-540-58156-1_68"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB10","doi-asserted-by":"crossref","unstructured":"A. Felty. Two-level meta-reasoning in Coq. To appear in Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, 2002.","DOI":"10.1007\/3-540-45685-6_14"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB11","unstructured":"J. Frost. A case study of co-induction in Isabelle. Technical Report 359, University of Cambridge, Computer Laboratory, Feb. 1995. Revised version of CUCL 308, August 1993."},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB12","doi-asserted-by":"crossref","unstructured":"M. Hofmann. Semantical analysis for higher-order abstract syntax. In G. Longo, editor, Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS'99), pages 204\u2013213, Trento, Italy, July 1999. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1999.782616"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB13","doi-asserted-by":"crossref","unstructured":"F. Honsell, M. Miculan, and I. Scagnetto. An axiomatic approach to metareasoning on systems in higher-order abstract syntax. In Proc. ICALP'01, number 2076 in LNCS, pages 963\u2013978. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-48224-5_78"},{"issue":"253","key":"10.1016\/S1571-0661(04)80506-1_NEWBIB14","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","article-title":"\u03c0-calculus in (co)inductive type theories","volume":"2","author":"Honsell","year":"2001","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.1016\/S1571-0661(04)80506-1_NEWBIB15","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1006\/inco.1996.0008","article-title":"Proving congruence of bisimulation in functional programming languages","volume":"124","author":"Howe","year":"1996","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB16","doi-asserted-by":"crossref","unstructured":"M. Gabbay and A. Pitts. A new approach to abstract syntax involving binders. In G. Longo, editor, Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS'99), pages 214\u2013224, Trento, Italy, 1999. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1999.782617"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB17","article-title":"Bisimulation in untyped lambda calculus: B\u00f6hm trees and bisimulation up to context","volume":"volume 20","author":"Lassen","year":"2000"},{"issue":"1","key":"10.1016\/S1571-0661(04)80506-1_NEWBIB18","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1145\/504077.504080","article-title":"Reasoning with higher-order abstract syntax in a logical framework","volume":"3","author":"McDowell","year":"2002","journal-title":"ACM Transactions on Computational Logic"},{"issue":"1-2","key":"10.1016\/S1571-0661(04)80506-1_NEWBIB19","first-page":"246","article-title":"Encoding transition systems in sequent calculus","volume":"197","author":"McDowell","year":"1998","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB20","unstructured":"James McKinna and Robert Pollack. Some lambda calculus and type theory formalized. To appear in Journal of Automated Reasoning, Special Issue on Formalized Mathematical Theories, ed. F. Pfenning."},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB21","unstructured":"M. Miculan. Developing (meta)theory of lambda-calculus in the theory of contexts. In S. Ambler, R. Crole, and A. Momigliano, editors, MERLIN 2001: Proceedings of the Workshop on MEchanized Reasoning about Languages with variable bINding, volume 58 of Electronic Notes in Theoretical Computer Science, pages 1\u201322, November 2001."},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB22","unstructured":"A. Momigliano, S. Ambler, and R. Crole. A comparison of formalizations of the meta-theory of a language with variable bindings in Isabelle. In Supplementary Proceedings of TPHOLs 2001, Edinburg University Technical Report, 2001."},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB23","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Sch\u00fcrmann. System description: Twelf \u2014 a meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202\u2013206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB24","unstructured":"A. M. Pitts. Operationally based theories of program equivalence. Technical report, Cambridge University Computer Laboratory, 1995. Notes to accompany lectures given at the Summer School on Semantics and Logics of Computation, Isaac Newton Institute for Mathematical Sciences, Cambridge, UK."},{"key":"10.1016\/S1571-0661(04)80506-1_NEWBIB25","unstructured":"C. Sch\u00fcrmann. Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, 2000. CMU-CS-00-146."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104805061?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104805061?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:05:55Z","timestamp":1761609955000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104805061"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,12]]}},"alternative-id":["S1571066104805061"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80506-1","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"A Hybrid Encoding of Howe's Method for Establishing Congruence of Bisimilarity","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80506-1","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}