{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:10Z","timestamp":1774837810575,"version":"3.50.1"},"publisher-location":"Berlin\/Heidelberg","reference-count":23,"publisher":"Springer-Verlag","isbn-type":[{"value":"3540565175","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037116","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"328-345","source":"Crossref","is-referenced-by-count":170,"title":["Inductive definitions in the system Coq rules and properties"],"prefix":"10.1007","author":[{"given":"Christine","family":"Paulin-Mohring","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Ph. Audebaud. Partial objects in the calculus of constructions. In Proceedings of the sixth Conf. on Logic in Computer Science. IEEE, 1991.","DOI":"10.1109\/LICS.1991.151633"},{"key":"23_CR2","unstructured":"Ph. Audebaud. Extension du Calcul des Constructions par Points fixes. PhD thesis, Universit\u00e9 Bordeaux I, 1992."},{"key":"23_CR3","unstructured":"H. Barendregt. Lambda calculi with types. Technical Report 91\u201319, Catholic University Nijmegen, 1991. in Handbook of Logic in Computer Science, Vol II."},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"C. B\u00f6hm and A. Berarducci. Automatic synthesis of typed \u03bb-programs on term algebras. Theoretical Computer Science, 39, 1985.","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"23_CR5","unstructured":"R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"23_CR6","unstructured":"Th. Coquand. Metamathematical investigations of a Calculus of Constructions. In P. Oddifredi, editor, Logic and Computer Science. Academic Press, 1990. Rapport de recherche INRIA 1088, also in [11]."},{"key":"23_CR7","unstructured":"Th. Coquand. Pattern matching with dependent types. In Nordstr\u00f6m et al. [17]."},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Th. Coquand and C. Paulin-Mohring. Inductively defined types. In P. Martin-L\u00f6f and G. Mints, editors, Proceedings of Colog'88. Springer-Verlag, 1990. LNCS 417.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"23_CR9","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/0167-6423(90)90058-L","volume":"14","author":"P. Dybjer","year":"1990","unstructured":"P. Dybjer. Comparing integrated and external logics of functional programs. Science of Computer Programming, 14:59\u201379, 1990.","journal-title":"Science of Computer Programming"},{"key":"23_CR10","unstructured":"G. Dowek et al. The Coq Proof Assistant User's Guide Version 5.6. Rapport Technique 134, INRIA, December 1991."},{"key":"23_CR11","unstructured":"G. Huet ed. The Calculus of Constructions, Documentation and user's guide, Version V4.10, 1989. Rapport technique INRIA 110."},{"key":"23_CR12","unstructured":"H. Geuvers. Type systems for Higher Order Logic. Faculty of Mathematics and Informatics, Catholic University Nijmegen, 1990."},{"key":"23_CR13","unstructured":"H. Geuvers and M.-J. Nederhof. A modular proof of strong normalization for the Calculus of Constructions. Faculty of Mathematics and Informatics, Catholic University Nijmegen, 1989."},{"key":"23_CR14","unstructured":"Z. Luo and R. Pollack. Lego proof development syste: User's manual. Technical Report ECS-LFCS-92-211, University of Edinburgh., 1992."},{"key":"23_CR15","unstructured":"L. Magnusson. The new implementation of ALF. In Nordstr\u00f6m et al. [17]."},{"key":"23_CR16","volume-title":"Recursive types and type constraints in second order lambda-calculus","author":"N. Mendler","year":"1987","unstructured":"N. Mendler. Recursive types and type constraints in second order lambda-calculus. In Symposium on Logic in Computer Science, Ithaca, NY, 1987. IEEE."},{"key":"23_CR17","unstructured":"B. Nordstr\u00f6m, K. Petersson, and G. Plotkin, editors. Proceedings of the 1992 Workshop on Types for Proofs and Programs, 1992."},{"key":"23_CR18","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Studies in Proof Theory. Bibliopolis, 1984."},{"key":"23_CR19","series-title":"volume 440 of LNCS","volume-title":"CSL'89","author":"M. Parigot","year":"1989","unstructured":"M. Parigot. On the representation of data in lambda-calculus. In CSL'89, volume 440 of LNCS, Kaiserslautern, 1989. Springer-Verlag."},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting F \u03c9's programs from proofs in the Calculus of Constructions. In Association for Computing Machinery, editor, Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989.","DOI":"10.1145\/75277.75285"},{"key":"23_CR21","unstructured":"C. Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. PhD thesis, Universit\u00e9 Paris 7, January 1989."},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Paulin-Mohring. Inductively defined types in the Calculus of Constructions. In Proceedings of Mathematical Foundations of Programming Semantics, LNCS 442. Springer-Verlag, 1990. also technical report CMU-CS-89-209.","DOI":"10.1007\/BFb0040259"},{"key":"23_CR23","unstructured":"B. Werner. A normalization proof for an impredicative type system with large elimination over integers. In Nordstr\u00f6m et al. [17]."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037116.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T22:22:07Z","timestamp":1607552527000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037116"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0037116","relation":{},"subject":[]}}