{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:41Z","timestamp":1774837841702,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540617808","type":"print"},{"value":"9783540707226","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61780-9_64","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:25:46Z","timestamp":1330295146000},"page":"85-104","source":"Crossref","is-referenced-by-count":11,"title":["Automating inversion of inductive predicates in Coq"],"prefix":"10.1007","author":[{"given":"Cristina","family":"Cornes","sequence":"first","affiliation":[]},{"given":"Delphine","family":"Terrasse","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"7_CR1","unstructured":"P. Aczel: An Introduction to Inductive Definitions. The Handbook of Mathematical Logic, J. Barwise ed., North-Holland, (1992) 739\u2013782"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"L. Augustsson: Compiling Pattern Matching. In J.P. Jouannaud, ed., Conference on Functional Programming Languages and Computer Architecture (LNCS 201), pages, 368\u2013381, Nancy, France, 1985.","DOI":"10.1007\/3-540-15975-4_48"},{"key":"7_CR3","first-page":"293","volume-title":"Logic and Databases","author":"K. Clark","year":"1978","unstructured":"K. Clark: Negation as Failure. Logic and Databases, Ed.H. Gallaire, J.Minker. Plenum Press New York, pp.293\u2013322, 1978."},{"key":"7_CR4","unstructured":"T. Coquand: Pattern Matching with Dependent Types. Informal Proceedings Types for Proofs and Programs, June 1992."},{"key":"7_CR5","unstructured":"T. Coquand, J.M.Smith: What is the status of pattern matching in type theory. El Winterm\u00f6te, pp.112\u2013114, June 1993."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"T. Coquand, G. Huet: The Calculus of Constructions. Information and Computation. Vol. 76, Nos. 2\/3, February\/March 1988.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"7_CR7","unstructured":"C. Cornes: Inversion des Pr\u00e9dicats Inductifs. Universit\u00e9 Paris VII, Rapport de stage de DEA Informatique Fondamentale. 1993."},{"key":"7_CR8","unstructured":"C. Cornes et al: The Coq Proof Assistant Reference Manual, Version 5.10. Projet Coq, Inria-Rocquencourt and CNRS-ENS Lyon, France."},{"key":"7_CR9","unstructured":"C. Cornes, D. Terrasse: Inverting Inductive Predicates in Coq. Rapport de Recherche I.N.R.I.A. to appear."},{"key":"7_CR10","first-page":"39","volume":"996","author":"E. Gim\u00e9nez","year":"1994","unstructured":"E. Gim\u00e9nez: Codifying guarded definitions with recursive schemes. In BRA Workshop on Types for Proofs and Programs, June 1994. LNCS 996 (1994) 39\u201359.","journal-title":"LNCS"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"E. Gim\u00e9nez: The implementation of coinductive types in Coq: an experiment with the Alternating Bit Protocol. In BRA Workshop Types for Proofs and Programs, Turin, June 1995. To appear in the LNCS series.","DOI":"10.1007\/3-540-61780-9_67"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Z. Luo: Computation and Reasoning: A Type Theory for Computer Science. 1994. Oxford University Press.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"7_CR13","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0304-3975(94)00021-2","volume":"135","author":"P. Manoury","year":"1994","unstructured":"P. Manoury, M. Simonot: Automatizing Termination Proofs of Recursively Defined Functions. Theoretical Computer Science. Vol. 135, pp.319\u2013343, 1994.","journal-title":"Theoretical Computer Science"},{"key":"7_CR14","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00f6f","year":"1984","unstructured":"P. Martin-L\u00f6f: Intuitionistic Type Theory. Bibliopolis, Napoli, 1984."},{"key":"7_CR15","first-page":"328","volume":"664","author":"C. Paulin-Mohring","year":"1992","unstructured":"Ch. Paulin-Mohring: Inductive Definitions in the System Coq: Rules and Properties. Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA), Springer-Verlag LNCS 664 (1992) 328\u2013345.","journal-title":"Springer-Verlag LNCS"},{"key":"7_CR16","unstructured":"T. Streicher: Semantical Investigations into Intensional Type Theory. LMU M\u00fcnchen. Habilitationsschrift. 1993"},{"key":"7_CR17","unstructured":"B. Werner: Une Th\u00e9orie des Constructions Inductives. Th\u00e8se Universit\u00e9 Paris VII, May 1994."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61780-9_64.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:47:30Z","timestamp":1713635250000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61780-9_64"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617808","9783540707226"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-61780-9_64","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}