{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:57Z","timestamp":1780994577333,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540626886","type":"print"},{"value":"9783540684381","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62688-3_34","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:48:25Z","timestamp":1330296505000},"page":"147-163","source":"Crossref","is-referenced-by-count":36,"title":["Primitive recursion for higher-order abstract syntax"],"prefix":"10.1007","author":[{"given":"Jo\u00eblle","family":"Despeyroux","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carsten","family":"Sch\u00fcrmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"10_CR2","first-page":"203","volume":"52","author":"T. Coquand","year":"1994","unstructured":"Thierry Coquand, Bengt Nordstr\u00f6m, Jan M. Smith, and Bj\u00f6rn von Sydow. Type theory and programming. Bulletin of the European Association for Theoretical Computer Science, 52:203\u2013228, February 1994.","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"10_CR3","first-page":"258","volume-title":"A modal analysis of staged computation","author":"R. Davies","year":"1996","unstructured":"Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Jr. Guy Steele, editor, Proceedings of the 23rd Annual Symposium on Principles of Programming Languages, pages 258\u2013270, St. Petersburg Beach, Florida, January 1996. ACM Press."},{"key":"10_CR4","series-title":"LNCS 902","first-page":"124","volume-title":"Higher-order abstract syntax in Coq","author":"J. Despeyroux","year":"1995","unstructured":"Jo\u00eblle Despeyroux, Amy Felty, and Andr\u00e9 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, April 1995. Springer-Verlag LNCS 902."},{"key":"10_CR5","series-title":"LNAI 822","first-page":"159","volume-title":"Higher-order abstract syntax with induction in Coq","author":"J. Despeyroux","year":"1994","unstructured":"Jo\u00eblle Despeyroux and Andr\u00e9 Hirschowitz. Higher-order abstract syntax with induction in Coq. In Frank Pfenning, editor, Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, pages 159\u2013173, Kiev, Ukraine, July 1994. Springer-Verlag LNAI 822."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Jo\u00eblle Despeyroux, Frank Pfenning, and Carsten Sch\u00fcrmann. Primitive recursion for higher-order abstract syntax. Technical Report CMU-CS-96-172, Carnegie Mellon University, September 1996.","DOI":"10.1007\/3-540-62688-3_34"},{"key":"10_CR7","unstructured":"Thierry Despeyroux and Andr\u00e9 Hirschowitz. Some theory for abstract syntax and induction. Draft manuscript."},{"key":"10_CR8","first-page":"284","volume-title":"Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space)","author":"L. Fegaras","year":"1996","unstructured":"Leonidas Fegaras and Tim Sheard. Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space). In Proceedings of 23rd Annual Symposium on Principles of Programming Languages, pages 284\u2013294, St. Petersburg Beach, Florida, January 1996. ACM Press."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Kurt G\u00f6del. On an extension of finitary mathematics which has not yet been used. In Solomon Feferman et al., editors, Kurt G\u00f6del, Collected Works, Volume II, pages 271\u2013280. Oxford University Press, 1990.","DOI":"10.1093\/oso\/9780195147216.003.0022"},{"issue":"1","key":"10_CR10","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, January 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10_CR11","first-page":"350","volume-title":"A computation model for executable higher-order algebraic specification languages","author":"J. Jouannaud","year":"1991","unstructured":"Jean-Pierre Jouannaud and Mitsuhiro Okada. A computation model for executable higher-order algebraic specification languages. In Gilles Kahn, editor, Proceedings of the 6th Annual Symposium on Logic in Computer Science, pages 350\u2013361, Amsterdam, The Netherlands, July 1991. IEEE Computer Society Press."},{"key":"10_CR12","unstructured":"Lena Magnusson. The Implementation of ALF\u2014A Proof Editor Based on Martin-L\u00f6f's Monomorphic Type Theory with Explicit Substitution. PhD thesis, Chalmers University of Technology and G\u00f6teborg University, January 1995."},{"key":"10_CR13","unstructured":"Raymond McDowell and Dale Miller. A logic for reasoning about logic specifications. Draft manuscript, July 1996."},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Erik Meijer and Graham Hutton. Bananas in space: Extending fold and unfold to exponential types. In Proceedings of the 7th Conference on Functional Programming Languages and Computer Architecture, La Jolla, California, June 1995.","DOI":"10.1145\/224164.224225"},{"key":"10_CR15","unstructured":"Dale Miller. An extension to ML to handle bound variables in data structures: Preliminary report. In Proceedings of the Logical Frameworks BRA Workshop, Nice, France, May 1990."},{"key":"10_CR16","first-page":"255","volume-title":"Eighth International Logic Programming Conference","author":"D. Miller","year":"1991","unstructured":"Dale Miller. Unification of simply typed lambda-terms as logic programming. In Koichi Furukawa, editor, Eighth International Logic Programming Conference, pages 255\u2013269, Paris, France, June 1991. MIT Press."},{"key":"10_CR17","series-title":"LNAI 592","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/3-540-55460-2_24","volume-title":"Abstract syntax and logic programming","author":"D. Miller","year":"1992","unstructured":"Dale Miller. Abstract syntax and logic programming. In Proceedings of the First and Second Russian Conferences on Logic Programming, pages 322\u2013337, Irkutsk and St. Petersburg, Russia, 1992. Springer-Verlag LNAI 592."},{"key":"10_CR18","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith. Programming in Martin-L\u00f6f's Type Theory: An Introduction, volume 7 of International Series of Monographs on Computer Science. Oxford University Press, 1990."},{"key":"10_CR19","first-page":"48","volume-title":"A functional theory of local names","author":"M. Odersky","year":"1994","unstructured":"Martin Odersky. A functional theory of local names. In Proceedings of the 21st Annual Symposium on Principles of Programming Languages, pages 48\u201359, Portland, Oregon, January 1994. ACM Press."},{"key":"10_CR20","series-title":"LNCS 664","first-page":"328","volume-title":"Inductive definitions in the system Coq: Rules and properties","author":"C. Paulin-Mohring","year":"1993","unstructured":"Christine 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, pages 328\u2013345, Utrecht, The Netherlands, March 1993. Springer-Verlag LNCS 664."},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Logic programming in the LF logical framework. In G\u00e9rard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 149\u2013181. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"10_CR22","volume-title":"To appear in Electronic Notes in Theoretical Computer Science, Volume 1","author":"F. Pfenning","year":"1995","unstructured":"Frank Pfenning and Hao-Chi Wong. On a modal \u03bb-calculus for S4. In S. Brookes and M. Main, editors, Proceedings of the Eleventh Conference on Mathematical Foundations of Programming Sematics, New Orleans, Louisiana, March 1995. To appear in Electronic Notes in Theoretical Computer Science, Volume 1, Elsevier."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62688-3_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:56:57Z","timestamp":1713635817000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62688-3_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540626886","9783540684381"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-62688-3_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}