{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:09:40Z","timestamp":1725487780014},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678632"},{"type":"electronic","value":"9783540446590"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_5","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T13:40:26Z","timestamp":1185025226000},"page":"73-89","source":"Crossref","is-referenced-by-count":4,"title":["Recursive Families of Inductive Types"],"prefix":"10.1007","author":[{"given":"Venanzio","family":"Capretta","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"H. P. Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Volume 2, pages 117\u2013309. Oxford University Press, 1992."},{"key":"5_CR2","unstructured":"Bruno Barras, Samuel Boutin, Cristina Cornes, Judica\u00ebl Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filli\u00e2tre, Eduardo Gim\u00e9nez, Hugo Herbelin, G\u00e9rard Huet, Henri Laulh\u00e8re, C\u00e9sar Mu\u00f1oz, Chetan Murthy, Catherine Parent-Vigouroux, Patrick Loiseleur, Christine Paulin-Mohring, Amokrane Sa\u00efbi, and Benjanin Werner. The Coq Proof Assistant Reference Manual. Version 6.3. INRIA, 1999."},{"key":"5_CR3","unstructured":"Bruno Barras and Benjamin Werner. Coq in Coq. Draft paper, 2000."},{"key":"5_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/BFb0014042","volume-title":"Types for Proofs and Programs (TYPES\u201995)","author":"G. Barthe","year":"1995","unstructured":"G. Barthe, M. Ruys, and H. P. Barendregt. A two-level approach towards lean proof-checking. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs (TYPES\u201995), volume 1158 of LNCS, pages 16\u201335. Springer, 1995."},{"key":"5_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software. Third International Symposium, TACS\u201997","author":"S. Boutin","year":"1997","unstructured":"Samuel Boutin. Using reflection to build efficient and certified decision procedures. In Mart\u00edn Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software. Third International Symposium, TACS\u201997, volume 1281 of LNCS, pages 515\u2013529. Springer, 1997."},{"key":"5_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/3-540-48256-3_10","volume-title":"Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs\u2019 99","author":"V. Capretta","year":"1999","unstructured":"Venanzio Capretta. Universal algebra in type theory. In Yves Bertot, Gilles Dowek, Andr\u00e9 Hirschowits, Christine Paulin, and Laurent Th\u00e9ry, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs\u2019 99, volume 1690 of LNCS, pages 131\u2013148. Springer-Verlag, 1999."},{"key":"5_CR7","unstructured":"Venanzio Capretta. Equational reasoning in type theory. \n                  http:\/\/www.cs.kun.nl\/~venanzio\n                  \n                , 2000."},{"key":"5_CR8","unstructured":"Thierry Coquand. An analysis of Girard\u2019s paradox. In Proceedings, Symposium on Logic in Computer Science, pages 227\u2013236, Cambridge, Massachusetts, 16\u201318 June 1986. IEEE Computer Society."},{"key":"5_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of Colog\u2019 88","author":"T. Coquand","year":"1990","unstructured":"Thierry Coquand and Christine Paulin. Inductively defined types. In P. Martin-L\u00f6f, editor, Proceedings of Colog\u2019 88, volume 417 of LNCS. Springer-Verlag, 1990."},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/S0304-3975(96)00145-4","volume":"176","author":"P. Dybjer","year":"1997","unstructured":"Peter Dybjer. Representing Inductively Defined Sets by Wellorderings in Martin-L\u00f6f Type Theory. Theoretical Computer Science, 176:329\u2013335, 1997.","journal-title":"Theoretical Computer Science"},{"key":"5_CR11","unstructured":"Herman Geuvers. Inductive and coinductive types with iteration and recursion. In Bengt Nordstr\u00f6m, Kent Pettersson, and Gordon Plotkin, editors, Proceedings of the 1992 Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden, June 1992, pages 193\u2013217, 1992. \n                  ftp:\/\/ftp.cs.chalmers.se\/pub\/cs-reports\/baastad.92\/proc.dvi.Z\n                  \n                ."},{"key":"5_CR12","unstructured":"Eduardo Gim\u00e9nez. A Tutorial on Recursive Types in Coq. Technical Report 0221, Unit\u00e9 de recherche INRIA Rocquencourt, May 1998."},{"key":"5_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/BFb0012835","volume-title":"9th International Conference on Automated Deduction","author":"D. J. Howe","year":"1988","unstructured":"Douglas J. Howe. Computational metatheory in Nuprl. In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction, volume 310 of LNCS, pages 238\u2013257. Springer-Verlag, 1988."},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI, 1979, pages 153\u2013175. North-Holland, 1982.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"5_CR15","unstructured":"Per Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980."},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1051\/ita:1999120","volume":"33","author":"R. Matthes","year":"1999","unstructured":"Ralph Matthes. Monotone (co)inductive types and positive fixed-point types. Theoretical Informatics and Applications, 33:309\u2013328, 1999.","journal-title":"Theoretical Informatics and Applications"},{"key":"5_CR17","volume-title":"Inductive Definition in Type Theory","author":"P. F. Mendler","year":"1987","unstructured":"Paul Francis Mendler. Inductive Definition in Type Theory. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, 1987."},{"key":"5_CR18","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith. Programming in Martin-L\u00f6f\u2019s Type Theory. Clarendon Press, 1990."},{"key":"5_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116","volume-title":"Proceedings of the conference Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring. Inductive Definitions in the System Coq-Rules and Properties. In M. Bezem and J.-F. Groote, editors, Proceedings of the conference Typed Lambda Calculi and Applications, volume 664 of LNCS, 1993. LIP research report 92-49."},{"key":"5_CR20","series-title":"Lect Notes Comput Sci","first-page":"54","volume-title":"Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs\u2019 99","author":"H. Pfeifer","year":"1999","unstructured":"Holger Pfeifer and Harals Rue\u03b2. Polytypic proof construction. In Yves Bertot, Gilleds Dowek, Andr\u00e9 Hirschowits, Christine Paulin, and Laurent Th\u00e9ry, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs\u2019 99, volume 1690 of LNCS, pages 54\u201372. Springer-Verlag, 1999."},{"key":"5_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0040259","volume-title":"Proceedings of Mathematical Foundations of Programming Semantics","author":"F. Pfenning","year":"1990","unstructured":"F. Pfenning and C. Paulin-Mohring. Inductively defined types in the Calculus of Constructions. In Proceedings of Mathematical Foundations of Programming Semantics, volume 442 of LNCS. Springer-Verlag, 1990. technical report CMU-CS-89-209."},{"key":"5_CR22","unstructured":"Mark Ruys. Studies in Mechanical Verification of Mathematical Proofs. PhD thesis, Computer Science Institute, University of Nijmegen, 1999."},{"key":"5_CR23","unstructured":"Milena Stefanova. Properties of Typing Systems. PhD thesis, Computing Science Institute, University of Nijmegen, 1999."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44659-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,18]],"date-time":"2019-02-18T01:33:23Z","timestamp":1550453603000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}