{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:35Z","timestamp":1774837835887,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540440390","type":"print"},{"value":"9783540456858","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_3","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T20:47:53Z","timestamp":1179607673000},"page":"13-30","source":"Crossref","is-referenced-by-count":17,"title":["Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction"],"prefix":"10.1007","author":[{"given":"Simon J.","family":"Ambler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roy L.","family":"Crole","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Momigliano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"3_CR1","series-title":"Lect Notes Comput Sci","first-page":"414","volume-title":"International Workshop on Higher Order Logic Theorem Proving and its Applications","author":"A. Gordon","year":"1993","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."},{"key":"3_CR2","unstructured":"S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65\u2013116. Addison-Wesley, 1990."},{"key":"3_CR3","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"},{"issue":"5","key":"3_CR4","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. Bruijn de","year":"1972","unstructured":"N. de Bruijn. Lambda-calculus notation with nameless dummies: A tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math., 34(5):381\u2013392, 1972.","journal-title":"Indag. Math."},{"key":"3_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/BFb0014049","volume-title":"Proceedings of the International Conference on Typed Lambda Calculi and Applications","author":"J. Despeyroux","year":"1995","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."},{"key":"3_CR6","unstructured":"J. Despeyroux and P. Leleu. Metatheoretic results for a modal \u03bb-calculus. Journal of Functional and Logic Programming, 2000(1), 2000."},{"key":"3_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-62688-3_34","volume-title":"Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA\u2019 97)","author":"J. Despeyroux","year":"1997","unstructured":"J. Despeyroux, F. Pfenning, and C. Sch\u00fcrmann. Primitive recursion for higher-order abstract syntax. In R. Hindley, editor, Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA\u2019 97), pages 147\u2013163, Nancy, France, Apr. 1997. Springer-Verlag LNCS."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"M. Fiore, G.D. Plotkin, and D. Turi. Abstract Syntax and Variable Binding. In G. Longo, editor, Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS\u201999), pages 193\u2013202, Trento, Italy, 1999. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1999.782615"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"J. Ford and I.A. Mason. Operational Techniques in PVS-A Preliminary Evaluation. In Proceedings of the Australasian Theory Symposium, CATS\u2019 01, 2001.","DOI":"10.1016\/S1571-0661(04)80882-X"},{"key":"3_CR10","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\u201999), pages 214\u2013224, Trento, Italy, 1999. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1999.782617"},{"key":"3_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001","author":"S. Gay","year":"2001","unstructured":"S. Gay. A framework for the formalisation of pi-calculus type systems in Isabelle\/HOL. In Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001, LNCS. Springer-Verlag, 2001."},{"key":"3_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BFb0105404","volume-title":"Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201996)","author":"A.D. Gordon","year":"1996","unstructured":"A.D. Gordon and T. Melham. Five axioms of alpha-conversion. In J. von Wright, J. Grundy, and J. Harrison, editors, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201996), volume 1125 of Lecture Notes in Computer Science, pages 173\u2013190, Turku, Finland, August 1996. Springer-Verlag."},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"E.L. Gunter. Why we can\u2019t have SML style datatype declarations in HOL. In L.J.M. Claese and M.J.C. Gordon, editors, Higher Order Logic Theorem Proving and Its Applications, volume A-20 of IFIP Transactions, pages 561\u2013568. North-Holland Press, Sept. 1992.","DOI":"10.1016\/B978-0-444-89880-7.50042-5"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"L. Hallnas. Partial inductive definitions. Theoretical Computer Science, 87(1):115\u2013147, July 1991.","DOI":"10.1016\/S0304-3975(06)80007-1"},{"issue":"1","key":"3_CR15","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, Jan. 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"3_CR16","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\u201999), pages 204\u2013213, Trento, Italy, July 1999. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1999.782616"},{"key":"3_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"963","DOI":"10.1007\/3-540-48224-5_78","volume-title":"Proc. ICALP 2001","author":"F. Honsell","year":"2001","unstructured":"F. Honsell, M. Miculan, and I. Scagnetto. An axiomatic approach to metareasoning on systems in higher-order abstract syntax. In Proc. ICALP 2001, volume 2076 in LNCS, pages 963\u2013978. Springer-Verlag, 2001."},{"issue":"253","key":"3_CR18","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"2","author":"F. Honsell","year":"2001","unstructured":"F. Honsell, M. Miculan, and I. Scagnetto. \u03c0-calculus in (co)inductive type theories. Theoretical Computer Science, 2(253):239\u2013285, 2001.","journal-title":"Theoretical Computer Science"},{"key":"3_CR19","unstructured":"R. McDowell. Reasoning in a Logic with Definitions and Induction. PhD thesis, University of Pennsylvania, 1997."},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"R. McDowell and D. Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Transaction in Computational Logic, 2001. To appear.","DOI":"10.1145\/504077.504080"},{"key":"3_CR21","unstructured":"J. McKinna and R. Pollack. Some Type Theory and Lambda Calculus Formalised. To appear in Journal of Automated Reasoning, Special Issue on Formalised Mathematical Theories (F. Pfenning, Ed.)"},{"issue":"1","key":"3_CR22","first-page":"50","volume":"1","author":"T.F. Melham","year":"1994","unstructured":"T.F. Melham. A mechanized theory of the \u03c0-calculus in HOL. Nordic Journal of Computing, 1(1):50\u201376, Spring 1994.","journal-title":"Nordic Journal of Computing"},{"key":"3_CR23","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 Scienc, pages 1\u201322, November 2001."},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"J. Parrow. An introduction to the pi-calculus. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, pages 479\u2013543. Elsevier Science, 2001.","DOI":"10.1016\/B978-044482830-9\/50026-6"},{"key":"3_CR25","unstructured":"F. Pfenning. Computation and deduction. Lecture notes, 277 pp. Revised 1994, 1996, to be published by Cambridge University Press, 1992."},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN\u201988 Symposium on Language Design and Implementation, pages 199\u2013208, Atlanta, Georgia, June 1988.","DOI":"10.1145\/53990.54010"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Sch\u00fcrmann. System description: Twelf\u2014 A metalogical 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":"3_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/3-540-45500-0_11","volume-title":"Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29\u201331, 2001, Proceedings","author":"A. M. Pitts","year":"2001","unstructured":"A. M. Pitts. Nominal logic: A first order theory of names and binding. In N. Kobayashi and B. C. Pierce, editors, Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29\u201331, 2001, Proceedings, volume 2215 of Lecture Notes in Computer Science, pages 219\u2013242. Springer-Verlag, Berlin, 2001."},{"key":"3_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/3-540-45127-7_23","volume-title":"Proceedings of RTA 2001","author":"R. Vestergaard","year":"2001","unstructured":"R. Vestergaard and J. Brotherson. A formalized first-order conflence proof for the \u03bb-calculus using one sorted variable names. In A. Middelrop, editor, Proceedings of RTA 2001, volume 2051 of LNCS, pages 306\u2013321. Springer-Verlag, 2001."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T05:38:22Z","timestamp":1556429902000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}