{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:11Z","timestamp":1761611171569},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540590484"},{"type":"electronic","value":"9783540491781"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014049","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:50:31Z","timestamp":1132732231000},"page":"124-138","source":"Crossref","is-referenced-by-count":60,"title":["Higher-order abstract syntax in Coq"],"prefix":"10.1007","author":[{"given":"Jo\u00eblle","family":"Despeyroux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amy","family":"Felty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e9","family":"Hirschowitz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"9_CR1","unstructured":"A. Asperti and G. Longo. Categories, Types, and Structures. MIT Press, Foundations of Computing Series, London, England, 1991."},{"issue":"3","key":"9_CR2","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/BF00245294","volume":"9","author":"A. Avron","year":"1992","unstructured":"A. Avron, F. Honsell, I. A. Mason, and R. Pollack. Using typed lambda calculus to implement formal systems on a machine. Journal of Automated Reasoning, 9(3):309\u2013354, Dec. 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR3","unstructured":"J. Despeyroux and A. Hirschowitz. Higher-order syntax and induction in coq. In Proceedings of the fifth Int. Conf. on Logic Programming and Automated Reasoning (LPAR 94), Kiev, Ukraine, July 16\u201321, 1994, 1994. Also available as an INRIA Research Report RR-2292, Inria-Sophia-Antipolis, France, June 1994."},{"key":"9_CR4","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The coq proof assistant user's guide. Technical Report 154, INRIA, 1993."},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"A. Felty. A logic programming approach to implementing higher-order term rewriting. In L.-H. Eriksson, L. Halln\u00e4s, and P. Schroeder-Heister, editors, Proceedings of the January 1991 Workshop on Extensions to Logic Programming, pages 135\u2013161. Springer-Verlag LNCS, 1992.","DOI":"10.1007\/BFb0013606"},{"issue":"1","key":"9_CR6","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/BF00881900","volume":"11","author":"A. Felty","year":"1993","unstructured":"A. Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11(1):43\u201381, Aug. 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR7","unstructured":"J. Hannan. Investigating a Proof-Theoretic Meta-Language for Functional Programs. PhD thesis, University of Pennsylvania, Technical Report MS-CIS-91-09, Jan. 1991."},{"key":"9_CR8","doi-asserted-by":"crossref","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:415\u2013459, 1992.","journal-title":"Mathematical Structures in Computer Science"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"J. Hannan and F. Pfenning. Compiler verification in LF. In Seventh Annual Symposium on Logic in Computer Science, pages 407\u2013418, 1992.","DOI":"10.1109\/LICS.1992.185552"},{"issue":"1","key":"9_CR10","doi-asserted-by":"publisher","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 denning logics. Journal of the ACM, 40(1):143\u2013184, Jan. 1993.","journal-title":"Journal of the ACM"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"S. Michaylov and F. Pfenning. Natural semantics and some of its meta-theory in elf. In L.-H. Eriksson, L. Halln\u00e4s, and P. Schroeder-Heister, editors, Proceedings of the January 1991 Workshop on Extensions to Logic Programming, pages 299\u2013344. Springer-Verlag LNCS, 1992.","DOI":"10.1007\/BFb0013612"},{"key":"9_CR12","unstructured":"D. Miller. Unification of simply typed lambda-terms as logic programming. In Eighth International Logic Programming Conference. MIT Press, 1991."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Inductive definitions in the system Coq; rules and properties. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, volume 664, pages 328\u2013345. Springer Verlag Lecture Notes in Computer Science, 1993.","DOI":"10.1007\/BFb0037116"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"F. Pfenning and E. Rohwedder. Implementing the meta-theory of deductive systems. In Eleventh International Conference on Automated Deduction, pages 537\u2013551. Springer-Verlag LNCS, 1992.","DOI":"10.1007\/3-540-55602-8_190"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014049","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,5]],"date-time":"2019-02-05T10:37:45Z","timestamp":1549363065000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014049"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590484","9783540491781"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0014049","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}