{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:23:23Z","timestamp":1725665003128},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540626886"},{"type":"electronic","value":"9783540684381"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62688-3_32","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:49:08Z","timestamp":1330296548000},"page":"112-128","source":"Crossref","is-referenced-by-count":7,"title":["A module calculus for pure type systems"],"prefix":"10.1007","author":[{"given":"Judica\u00ebl","family":"Courant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"8_CR1","unstructured":"Mar\u00eda Virginia Aponte and Giuseppe Castagna. Programmation modulaire avec surcharge et liaison tardive. In Journ\u00e9es Francophonesdes Langages Applicatifs, January 1996."},{"key":"8_CR2","unstructured":"H. Barendregt. Lambda calculi with types. Technical Report 91-19, Catholic University Nijmegen, 1991. in Handbook of Logic in Computer Science, Vol II."},{"key":"8_CR3","volume-title":"Th\u00e9orie des Ensembles","author":"N. Bourbaki","year":"1970","unstructured":"Nicolas Bourbaki. El\u00e9ments de Math\u00e9matique; Th\u00e9orie des Ensembles, chapter IV. Hermann, Paris, 1970."},{"key":"8_CR4","unstructured":"C. Cornes, J. Courant, J.-C. Filli\u00e2tre, G. Huet, P. Manoury, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Sa\u00efbi, and B. Werner. The Coq Proof Assistant Reference Manual Version 5.10. Technical Report 0177, INRIA, July 1995."},{"key":"8_CR5","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The Calculus of Constructions. Inf. Comp., 76:95\u2013120, 1988.","journal-title":"Inf. Comp."},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"CiME: Completion Modulo E","author":"E. Contejean","year":"1996","unstructured":"Evelyne Contejean and Claude March\u00e9. CiME: Completion Modulo E. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science. Springer-Verlag, Rutgers University, NJ, USA, July 1996."},{"key":"8_CR7","unstructured":"Judica\u00ebl Courant. A module calculus enjoying the subject-reduction property. Research Report RR 96-30, LIP, 1996. Preliminary version."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Roberto Di Cosmo. Isomorphisms of types: from \u03bb-calculus to information retrieval and language design. Progress in Theoretical Computer Science. Birkhauser, 1995. ISBN-0-8176-3763-X.","DOI":"10.1007\/978-1-4612-2572-0"},{"key":"8_CR9","unstructured":"William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. The IMPS User's Manual. The MITRE Corporation, first edition, version 2 edition, 1995."},{"issue":"1","key":"8_CR10","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143\u2013184, January 1993. Preliminary version appeared in Proc. 2nd IEEE Symposium on Logic in Computer Science, 1987,194\u2013204.","journal-title":"Journal of the ACM"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In 21st Symposium on Principles of Programming Languages, pages 123\u2013137. ACM Press, 1994.","DOI":"10.1145\/174675.176927"},{"key":"8_CR12","volume-title":"Technical Report CMU-CS-92-191","author":"R. Harper","year":"1992","unstructured":"Robert Harper and Frank Pfenning. A module system for a programming language based on the LF logical framework. Technical Report CMU-CS-92-191, Carnegie Mellon University, Pittsburgh, Pennsylvania, September 1992."},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Mark P. Jones. Using parameterized signatures to express modular structures. In 23rd Symposium on Principles of Programming Languages. ACM Press, 1996. To appear.","DOI":"10.1145\/237721.237731"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Xavier Leroy. Manifest types, modules, and separate compilation. In 21st symp. Principles of Progr. Lang., pages 109\u2013122. ACM Press, 1994.","DOI":"10.1145\/174675.176926"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Xavier Leroy. Applicative functors and fully transparent higher-order modules. In 22nd Symposium on Principles of Programming Languages, pages 142\u2013153. ACM Press, 1995.","DOI":"10.1145\/199448.199476"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Zhaohui Luo. ECC: an Extended Calculus of Constructions. In Proc. of IEEE 4th Ann. Symp. on Logic In Computer Science, Asilomar, California, 1989.","DOI":"10.1109\/LICS.1989.39193"},{"key":"8_CR17","unstructured":"David B. MacQueen. Modules for Standard ML. Polymorphism, 2(2), 1985. 35 pages. An earlier version appeared in Proc. 1984 ACM Conf. on Lisp and Functional Programming."},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Lena Magnusson and Bengt Nordstr\u00f6m. The ALF proof editor and its proof engine. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, pages 213\u2013237. Springer-Verlag LNCS 806,1994.","DOI":"10.1007\/3-540-58085-9_78"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Inductive definitions in the system Coq: Rules and Properties. In M. Bezem, J.F. Groote, editor, Proceedings of the TLCA, 1993.","DOI":"10.1007\/BFb0037116"},{"key":"8_CR20","unstructured":"Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994."},{"key":"8_CR21","unstructured":"Fran\u00e7ois Rouaix. The Alcool 90 report. Technical report, INRIA, 1992. Included in the distribution available at ftp. inria. fr."},{"key":"8_CR22","unstructured":"Amokrane Saibi, 1996. Private Communication."},{"key":"8_CR23","unstructured":"Don Sannella. Formal program development in Extended ML for the working programmer. In Proc. 3rd BCS\/FACS Workshop on Refinement, pages 99\u2013130. Springer Workshops in Computing, 1990."},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"P. Severi and E. Poll. Pure type systems with definitions. Lecture Notes in Computer Science, 813, 1994.","DOI":"10.1007\/3-540-58140-5_30"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62688-3_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:14:02Z","timestamp":1605647642000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62688-3_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540626886","9783540684381"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-62688-3_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}