{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:45Z","timestamp":1749124065873},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651376"},{"type":"electronic","value":"9783540495628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097795","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T09:27:48Z","timestamp":1164360468000},"page":"236-253","source":"Crossref","is-referenced-by-count":9,"title":["Inverting inductively defined relations in LEGO"],"prefix":"10.1007","author":[{"given":"Conor","family":"McBride","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"R. M. Burstall. Inductively Defined Relations: A Brief Tutorial. Extended Abstract. In Haveraan, M., and Owe, O., and Dahl, O.-J. editors, Recent Trends in Data Types Specification. Springer LNCS 1130, pp14\u201317. 1996.","DOI":"10.1007\/3-540-61629-2_33"},{"key":"13_CR2","unstructured":"J. Camilleri and T. Melham. Reasoning with Inductively Defined Relations in the HOL Theorem Prover. Technical Report No. 265 University of Cambridge Computer Laboratory. 1992."},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"K. Clark. Negation as Failure. pp293\u2013322 of Logic and Data Bases, edited by H. Gallaire and J. Minker. Plenum Press. 1978.","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"13_CR4","unstructured":"C. Cornes, J. Courant, J.F. Filla\u00eetre, G. Huet, C. Murthy, C. Parent, C. Paulin, B. Werner. The Coq Proof Assistant Reference Manual, Version 5.10. Projet Coq, Inria-Rocquencourt and CNRS-ENS Lyon, France."},{"key":"13_CR5","unstructured":"C. Cornes Compilation du Filtrage avec Types D\u00e9pendants dans le Syst\u00e8me Coq. Actes de la r\u00e9union du p\u00f4le Sp\u00e9cification et Preuves du GDR Programmation. Orleans, Novembre 1996."},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"C. Cornes, D. Terrasse. Automating Inversion of Inductive Predicates in Coq. In BRA Workshop on Types for Proofs and Programs, Turin, June 1995. To appear in LNCS series.","DOI":"10.1007\/3-540-61780-9_64"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"L.-H. Eriksson. A finitary version of the calculus of partial inductive definitions. In: L.-H. Eriksson, L. Halln\u00e4s & P. Schroeder-Heister (editors), Extensions of Logic Programming. Second International Workshop, ELP-91, Stockholm. Springer LNCS 596, pp89\u2013134. 1992.","DOI":"10.1007\/BFb0013605"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"P. Dybjer. Inductive Sets and Families in Martin-L\u00f6f's Type Theory. pp280\u2013306 of Logical Frameworks, edited by G. Huet and G. Plotkin. CUP 1991.","DOI":"10.1017\/CBO9780511569807.012"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"E. Giminez. Codifying guarded definitions with recursive schemes. Proceedings of Types 94, pp39\u201359.","DOI":"10.1007\/3-540-60579-7_3"},{"key":"13_CR10","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/S0304-3975(06)80007-1","volume":"87","author":"L. Halln\u00e4s","year":"1991","unstructured":"L. Halln\u00e4s. Partial Inductive Definitions. Theoretical Computer Science. Vol. 87. pp115\u2013142. 1991.","journal-title":"Theoretical Computer Science"},{"key":"13_CR11","unstructured":"Introduction to HOL; A theorem proving environment for higher order logic. Edited by M.J.C. Gordon and T.F. Melham. CUP 1993."},{"key":"13_CR12","unstructured":"Jean-Pierre Jouannaud and Claude Kirchner. Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification. pp257\u2013321 of Computational Logic: Essays in Honor of Alan Robinson, edited by Jean-Louis Lassez and Gordon Plotkin, MIT Press, 1991."},{"key":"13_CR13","unstructured":"Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. OUP 1994."},{"key":"13_CR14","unstructured":"Zhaohui Luo, Randy Pollack. LEGO Proof Development System: User Manual. Technical Note, 1992."},{"key":"13_CR15","volume-title":"The Implementation of ALF","author":"L. Magnusson","year":"1995","unstructured":"Lena Magnusson. The Implementation of ALF. PhD Thesis. Chalmers University of Technology and University of G\u00f6teborg, Sweden. January 1995."},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"L. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge Tracts in Theoretical Computer Science 2. CUP 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"13_CR17","unstructured":"Randy Pollack. Incremental Changes in LEGO: Technical Note, 1994."},{"key":"13_CR18","volume-title":"Natural Deduction: A Proof-Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"Prawitz, D. Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell. Stockholm, 1965."},{"key":"13_CR19","unstructured":"H. Tamaki, T. Sato. Unfold\/Fold Transformation of Logic Programs. Proceedings of Second International Logic Programming Conference. pp127\u2013138. Uppsala, 1984."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097795","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T10:54:03Z","timestamp":1555930443000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097795"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0097795","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}