{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T06:10:27Z","timestamp":1737094227018,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008972"},{"type":"electronic","value":"9783540365761"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36576-1_24","type":"book-chapter","created":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T02:42:17Z","timestamp":1181616137000},"page":"375-391","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Multi-level Meta-reasoning with Higher-Order Abstract Syntax"],"prefix":"10.1007","author":[{"given":"Alberto","family":"Momigliano","sequence":"first","affiliation":[]},{"given":"Simon J.","family":"Ambler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"24_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Combining higher order abstract syntax with tactical theorem proving and (co)induction","author":"S. Ambler","year":"2002","unstructured":"S. Ambler, R. Crole, and A. Momigliano. Combining higher order abstract syntax with tactical theorem proving and (co)induction. In V. A. Carre\u00f1o, editor, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, volume 2342 of LNCS. Springer Verlag, 2002."},{"key":"24_CR2","unstructured":"S. Boutin. Proving correctness of the translation from mini-ML to the CAM with the Coq proof development system. Technical Report RR-2536, Inria, Institut National de Recherche en Informatique et en Automatique, 1995."},{"key":"24_CR3","unstructured":"B. Ciesielski and M. Wand. Using the theorem prover Isabelle-91 to verify a simple proof of compiler correctness. Technical Report NU-CCS-91-20, College of Computer Science, Northeastern University, Dec. 1991."},{"key":"24_CR4","unstructured":"J. Despeyroux. Proof of translation in natural semantics. In Proceedings of LICS\u201986, pages 193\u2013205, Cambridge, MA, 1986. IEEE Computer Society Press."},{"key":"24_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/BFb0014049","volume-title":"Higher-order abstract syntax in Coq.","author":"J. Despeyroux","year":"1995","unstructured":"J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-order abstract syntax in Coq. InM. 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":"24_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Two-level meta-reasoning in Coq","author":"A. Felty","year":"2002","unstructured":"A. Felty. Two-level meta-reasoning in Coq. In V. A. Carre\u00f1o, editor, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, volume 2342 of LNCS. Springer Verlag, 2002."},{"key":"24_CR7","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, 1999. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1999.782617"},{"issue":"1","key":"24_CR8","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/S0304-3975(06)80007-1","volume":"87","author":"L. Hallnas","year":"1991","unstructured":"L. Hallnas. Partial inductive definitions. TCS, 87(1):115\u2013147, July 1991.","journal-title":"TCS"},{"issue":"4","key":"24_CR9","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1017\/S0960129500001559","volume":"2","author":"J. Hannan","year":"1992","unstructured":"J. Hannan and D. Miller. From operational semantics to abstract machines. Mathematical Structures in Computer Science, 2(4):415\u2013459, 1992.","journal-title":"Mathematical Structures in Computer Science"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"J. Hannan and F. Pfenning. Compiler verification in LF. In A. Scedrov, editor, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 407\u2013418, Santa Cruz, California, June 1992.","DOI":"10.1109\/LICS.1992.185552"},{"issue":"4","key":"24_CR11","first-page":"517","volume":"33","author":"P. H. Hartel","year":"2001","unstructured":"P. H. Hartel and L. Moreau. Formalizing the safety of Java,the Java Virtual Machine, and Java Card. ACMCS, 33(4):517\u2013558, Dec. 2001.","journal-title":"ACMCS"},{"key":"24_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"963","DOI":"10.1007\/3-540-48224-5_78","volume-title":"An axiomatic approach to metareasoning on systems in higher-order abstract syntax","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\u201901, number 2076in LNCS, pages 963\u2013978. Springer-Verlag, 2001."},{"key":"24_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/BFb0022269","volume-title":"Computer Science Logic","author":"D. Lester","year":"1995","unstructured":"D. Lester and S. Mintchev. Towards machine-checked compiler correctness for higher-order pure functional languages. In L. Pacholski and J. Tiuryn, editors, Computer Science Logic, pages 369\u2013381. Springer-Verlag LNCS 933, 1995."},{"issue":"1","key":"24_CR14","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/504077.504080","volume":"3","author":"R. McDowell","year":"2002","unstructured":"R. McDowell and D. Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic, 3(1):80\u2013136, 2002.","journal-title":"ACM Transactions on Computational Logic"},{"key":"24_CR15","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125\u2013157, 1991.","journal-title":"Annals of Pure and Applied Logic"},{"key":"24_CR16","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0304-3975(91)90033-X","volume":"87","author":"R. Milner","year":"1991","unstructured":"R. Milner and M. Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87:209\u2013220, 1991.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"24_CR17","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/S1571-0661(04)80506-1","volume":"70","author":"Alberto Momigliano","year":"2002","unstructured":"A. Momigliano, S. Ambler, and R. Crole. A Hybrid encoding of Howe\u2019s method for establishing congruence of bisimilarity. ENTCS, 70(2), 2002.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"24_CR18","unstructured":"F. Pfenning. Computation and Deduction. Cambridge University Press, 2000. In preparation. Draft from April 1997 available electronically."},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"F. Pfenning and E. Rohwedder. Implementing the meta-theory of deductive systems. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction, pages 537\u2013551. Springer-Verlag LNAI 607.","DOI":"10.1007\/3-540-55602-8_190"},{"key":"24_CR20","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 CADE 16, pages 202\u2013206. Springer LNAI 1632.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"24_CR21","unstructured":"C. Sch\u00fcrmann. Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, 2000. CMU-CS-00-146."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36576-1_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:54:06Z","timestamp":1737093246000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36576-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008972","9783540365761"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-36576-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"28 February 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}