{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:56:36Z","timestamp":1725562596743},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540221647"},{"type":"electronic","value":"9783540248491"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24849-1_9","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T16:34:24Z","timestamp":1281285264000},"page":"130-146","source":"Crossref","is-referenced-by-count":8,"title":["Modules in Coq Are and Will Be Correct"],"prefix":"10.1007","author":[{"given":"Jacek","family":"Chrza\u0327szcz","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","first-page":"9","volume-title":"Sixteenth Annual IEEE Symposium on Logic in Computer Science","author":"F. Blanqui","year":"2001","unstructured":"Blanqui, F.: Definitions by rewriting in the calculus of constructions. In: Sixteenth Annual IEEE Symposium on Logic in Computer Science, Los Alamitos, USA, June 2001, pp. 9\u201318. IEEE Comp. Soc. Press, Los Alamitos (2001)"},{"key":"9_CR2","unstructured":"Blanqui, F.: Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science (2003) (to appear)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/10930755_18","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Chrza\u0327szcz","year":"2003","unstructured":"Chrza\u0327szcz, J.: Implementation of modules in the Coq system. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 270\u2013286. Springer, Heidelberg (2003)"},{"key":"9_CR4","unstructured":"Chrza\u0327szcz, J.: Modules in Type Theory with Generative Definitions. PhD thesis, Warsaw Univerity and University of Paris-Sud (January 2004), Available from http:\/\/www.mimuw.edu.pl\/~chrzaszc\/papers"},{"key":"9_CR5","unstructured":"The Coq proof assistant, http:\/\/coq.inria.fr\/"},{"key":"9_CR6","unstructured":"Coquand, T.: Pattern matching with dependent types. In: Proceedings of the Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden, pp. 71\u201383 (1992)"},{"key":"9_CR7","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Information and Computation\u00a076, 95\u2013120 (1988)","journal-title":"Information and Computation"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"COLOG-88","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417, Springer, Heidelberg (1990)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/3-540-62688-3_32","volume-title":"Typed Lambda Calculi and Applications","author":"J. Courant","year":"1997","unstructured":"Courant, J.: A Module Calculus for Pure Type Systems. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol.\u00a01210, pp. 112\u2013128. Springer, Heidelberg (1997)"},{"key":"9_CR10","unstructured":"Courant, J.: Un calcul de modules pour les syst\u00e8mes de types purs. Th\u00e8se de doctorat, Ecole Normale Sup\u00e9rieure de Lyon (1998)"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Harper, R., Lillibridge, M.: A type-theoretic approach to higher-order modules with sharing. In: POPL 1994 [17], pp. 123\u2013137.","DOI":"10.1145\/174675.176927"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Harper, R., Pfenning, F.: A module system for a programming language based on the LF logical framework. Journal of Logic and Computation\u00a01(8) (1998)","DOI":"10.1093\/logcom\/8.1.5"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Manifest types, modules, and separate compilation. In: POPL 1994 [17], pp. 109\u2013122.","DOI":"10.1145\/174675.176926"},{"key":"9_CR14","unstructured":"Luo, Z.: An Extended Calculus of Constructions. PhD thesis, University of Edinburgh (1990)"},{"key":"9_CR15","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. Computer Science Laboratory, SRI International, Menlo Park, CA (September 1999)"},{"key":"9_CR16","volume-title":"Logic and Computer Science","author":"L.C. Paulson","year":"1990","unstructured":"Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, Academic Press, London (1990)"},{"key":"9_CR17","unstructured":"Conference Record of the 21st Symposium on Principles of Programming Languages, Portland, Oregon. ACM Press, New York (1994)"},{"issue":"2","key":"9_CR18","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1017\/S0956796802004641","volume":"13","author":"D. Walukiewicz-Chrza\u0327szcz","year":"2003","unstructured":"Walukiewicz-Chrza\u0327szcz, D.: Termination of rewriting in the calculus of constructions. Journal of Functional Programming\u00a013(2), 339\u2013414 (2003)","journal-title":"Journal of Functional Programming"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Walukiewicz-Chrza\u0327szcz, D.: Termination of Rewriting in the Calculus of Constructions. PhD thesis, Warsaw University and University Paris XI (2003)","DOI":"10.1017\/S0956796802004641"},{"key":"9_CR20","unstructured":"Werner, B.: M\u00e9ta-th\u00e9orie du Calcul des Constructions Inductives. PhD thesis, Universit\u00e9 Paris 7 (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\/978-3-540-24849-1_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:57:44Z","timestamp":1605743864000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24849-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221647","9783540248491"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24849-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}