{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:18Z","timestamp":1761611298954},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540582168"},{"type":"electronic","value":"9783540485735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58216-9_36","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:34:59Z","timestamp":1330270499000},"page":"159-173","source":"Crossref","is-referenced-by-count":18,"title":["Higher-Order Abstract Syntax with induction in Coq"],"prefix":"10.1007","author":[{"given":"Jo\u00eblle","family":"Despeyroux","sequence":"first","affiliation":[]},{"given":"Andr\u00e9","family":"Hirschowitz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"12_CR1","unstructured":"A. Avron, F. Honsell, and A. Mason. Using typed \u03bb-calculus to implement formal systems on a machine. Technical Report ECS-LFCS-87-31, Edinburgh University, July 1987."},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Th. Despeyroux and A. Hirschowitz. A categorical approach to higher-order abstract syntax, forthcoming paper, 1994.","DOI":"10.1007\/3-540-58216-9_36"},{"key":"12_CR3","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, Ch. Paulin-Mohring, and B. Werner. The coq proof assistant user's guide, version 5.8. Technical Report 154, Inria, Rocquencourt, France, May 1993."},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"C. Elliot and F. Pfenning. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN' 88 International Conference on Programming Language Design and Implementation, Atlanta, Georgia, USA, June 22\u201324, 1988.","DOI":"10.1145\/53990.54010"},{"key":"12_CR5","unstructured":"J. Hannan and D. Miller. Enriching a meta-language with higher-order features. In Proceedings of the Workshop on Meta-Programming in Logic Programming, Bristol, June 1988."},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"J. Hannan and F. Pfenning. Compiler verification in LF. In IEEE, editor, Proceedings of the LICS International Conference on Logic In Computer Sciences, Santa Cruz, California, June 1992.","DOI":"10.1109\/LICS.1992.185552"},{"key":"12_CR7","volume-title":"Technical Report CMU-CS-90-144","author":"R. Harper","year":"1990","unstructured":"R. Harper. Systems of polymorphic type assignment in LF. Technical Report CMU-CS-90-144, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 1990."},{"key":"12_CR8","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. In IEEE, editor, Proceedings of the second LICS International Conference on Logic In Computer Sciences, Cornell, USA, pages 194\u2013204, 1987."},{"key":"12_CR9","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Technical Report ECS-LFCS-91-162, Edinburgh University, June 1991."},{"key":"12_CR10","unstructured":"G. Huet. Constructive computation theory. part I. Lecture notes. October 1992."},{"key":"12_CR11","unstructured":"G. Kahn. Natural semantics. In Proceedings of the Symp. on Theorical Aspects of Computer Science, Passau, Germany, 1987. also available as a Research Report RR-601, Inria, Sophia-Antipolis, February 1987."},{"key":"12_CR12","unstructured":"S. Michaylov and F. Pfenning. Natural semantics and some of its meta-theory in elf. In Lars Halln\"as, editor, Proceedings of the Second Workshop on Extentions of Logic Programing, Springer-Verlag LNCS, 1991. also available as a Technical Report MPI-I-91-211, Max-Planck-Institute for Computer Science,Saarbrucken, Germany, August 1991."},{"key":"12_CR13","unstructured":"D. Miller and G. Nadathur. An overview of \u03bb-prolog. In MIT Press, editor, Proceedings of the International Logic Programming Conference, Seattle, Washington, pages 910\u2013827, August 1988."},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Ch. Paulin-Mohring. Inductive definitions in the system coq. rules and properties. In J.F. Groote M. Bezem, editor, Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA'93, Springer-Verlag LNCS 664, pages 328\u2013345, 1992. also available as a Research Report RR-92-49, Dec. 1992, ENS Lyon, France.","DOI":"10.1007\/BFb0037116"},{"key":"12_CR15","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L. C. Paulson","year":"1989","unstructured":"L. C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363\u2013397, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Elf: A language for logic definition and verified metaprogramming. In Proceedings of the fourth ACM-IEEE Symp. on Logic In Computer Science, Asilomar, California, USA, June 1989.","DOI":"10.1109\/LICS.1989.39186"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"F. Pfenning and E. Rohwedder. Implementing the meta-theory of deductive systems. In Proceedings of the CADE-11 Conference, 1991.","DOI":"10.1007\/3-540-55602-8_190"}],"container-title":["Lecture Notes in Computer Science","Logic Programming and Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58216-9_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:18:39Z","timestamp":1605647919000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58216-9_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540582168","9783540485735"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-58216-9_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}