{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:25Z","timestamp":1775873545321,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540432876","type":"print"},{"value":"9783540458425","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45842-5_13","type":"book-chapter","created":{"date-parts":[[2007,5,26]],"date-time":"2007-05-26T20:00:38Z","timestamp":1180209638000},"page":"197-216","source":"Crossref","is-referenced-by-count":45,"title":["Elimination with a Motive"],"prefix":"10.1007","author":[{"given":"Conor","family":"McBride","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,2,14]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch. Extensional equality in intensional type theory. In LICS\u201999, 1999.","DOI":"10.1109\/LICS.1999.782636"},{"key":"13_CR2","unstructured":"Alan Bundy. The Automation Of Proof By Mathematical Induction. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science, 1999."},{"key":"13_CR3","unstructured":"L\u2019\u00c9quipe Coq. The Coq Proof Assistant Reference Manual. http:\/\/pauillac.inria.fr\/coq\/doc\/main.html , Apr 2001."},{"key":"13_CR4","unstructured":"Thierry Coquand. Pattern Matching with Dependent Types. In Proceedings of the Logical Framework workshop at B\u00e5stad, June 1992."},{"key":"13_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"International Conference on Computer Logic, LNCS 417","author":"T. Coquand","year":"1990","unstructured":"Thierry Coquand and Christine Paulin. Inductively defined types. In P. Martin-L\u00f6f and G. Mints, editors, COLOG-88. International Conference on Computer Logic, LNCS 417, pages 50\u201366. Springer-Verlag, 1990."},{"key":"13_CR6","unstructured":"Cristina Cornes. Conception d\u2019un langage de haut niveau de r\u00e9presenatation de preuves. PhD thesis, Universit\u00e9 Paris VII, 1997."},{"key":"13_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Types for Proofs and Programs\u201995","author":"C. Cornes","year":"1995","unstructured":"Cristina Cornes and Delphine Terrasse. Inverting Inductive Predicates in Coq. In Types for Proofs and Programs\u201995, LNCS 1158, Springer-Verlag, 1995."},{"key":"13_CR8","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0890-5401(91)90066-B","volume":"91","author":"N.G. Bruijn de","year":"1991","unstructured":"N.G. de Bruijn. Telescopic Mappings in Typed Lambda-Calculus. Information and Computation, 91:189\u2013204, 1991.","journal-title":"Information and Computation"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Peter Dybjer. Inductive Sets and Families inMartin-L\u00f6f\u2019s Type Theory. In G. Huet and G. Plotkin, editors, Logical Frameworks. CUP, 1991.","DOI":"10.1017\/CBO9780511569807.012"},{"key":"13_CR10","unstructured":"Martin Hofmann. Extensional concepts in intensional type theory. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh, 1995."},{"key":"13_CR11","unstructured":"Zhaohui Luo and Robert Pollack. LEGO Proof Development System: User\u2019s Manual. Technical Report ECS-LFCS-92-211, Laboratory for Foundations of Computer Science, University of Edinburgh, May 1992."},{"key":"13_CR12","unstructured":"Lena Magnusson. The implementation of ALF\u2014A Proof Editor based on Martin-L\u00f6f\u2019 s Monomorphic Type Theory with Explicit Substitutiton. PhD thesis, Chalmers University of Technology, G\u00f6teborg, 1994."},{"key":"13_CR13","unstructured":"Per Martin-L\u00f6f. A theory of types. manuscript, 1971."},{"key":"13_CR14","unstructured":"Per Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis\u00b7Napoli, 1984."},{"key":"13_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/BFb0097795","volume-title":"Types for Proofs and Programs\u201996","author":"C. McBride","year":"1998","unstructured":"Conor McBride. Inverting inductively defined relations in LEGO. In E. Gim\u00e9nez and C. Paulin-Mohring, editors, Types for Proofs and Programs\u201996, LNCS 1512, pages 236\u2013253, Springer-Verlag, 1998."},{"key":"13_CR16","unstructured":"Conor McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999."},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"J. McKinna. Deliverables: A Categorical Approach to Program Development in Type Theory. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh, 1992.","DOI":"10.1007\/3-540-57182-5_3"},{"issue":"4","key":"13_CR18","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"2","author":"D. Miller","year":"1991","unstructured":"Dale Miller. A Logic Programming Language with Lambda-Abstraction, Function Variables and Simple Unification. Journal of Logic and Computation, 2(4):497\u2013537, 1991.","journal-title":"Journal of Logic and Computation"},{"issue":"4","key":"13_CR19","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D. Miller","year":"1992","unstructured":"Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14(4):321\u2013358, 1992.","journal-title":"Journal of Symbolic Computation"},{"key":"13_CR20","unstructured":"Christine Paulin-Mohring. D\u00e9finitions Inductives en Th\u00e9orie des Types d\u2019Ordre Sup\u00e9rieur. Habilitation Thesis. Universit\u00e9 Claude Bernard (Lyon I), 1996."},{"key":"13_CR21","unstructured":"Robert Pollack. Implicit syntax."},{"key":"13_CR22","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"A. Robinson","year":"1965","unstructured":"Alan Robinson. A Machine-oriented Logic Based on the Resolution Principle. Journal of the ACM, 12:23\u201341, 1965.","journal-title":"Journal of the ACM"},{"key":"13_CR23","unstructured":"Thomas Streicher. Investigations into intensional type theory. Habilitation Thesis, Ludwig Maximilian Universit\u00e4t, 1993."},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"P. Wadler. Views: A way for pattern matching to cohabit with data abstraction. In POPL\u201987. ACM, 1987.","DOI":"10.1145\/41625.41653"}],"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-45842-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T07:03:01Z","timestamp":1556434981000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45842-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540432876","9783540458425"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45842-5_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}