{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:19Z","timestamp":1774837819599,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540406648","type":"print"},{"value":"9783540451303","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/10930755_18","type":"book-chapter","created":{"date-parts":[[2006,6,19]],"date-time":"2006-06-19T15:27:09Z","timestamp":1150730829000},"page":"270-286","source":"Crossref","is-referenced-by-count":28,"title":["Implementing Modules in the Coq System"],"prefix":"10.1007","author":[{"given":"Jacek","family":"Chrz\u0105szcz","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Chrza\u0327aszcz, J.: Modules in type theory with generative definitions. PhD thesis, to be defended (2003)"},{"key":"18_CR2","unstructured":"The Coq Proof Assistant, \n                    \n                      http:\/\/coq.inria.fr\/"},{"key":"18_CR3","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 1997","author":"J. Courant","year":"1997","unstructured":"Courant, J.: A Module Calculus for Pure Type Systems. In: Typed Lambda Calculi and Applications 1997. LNCS, pp. 112\u2013128. Springer, Heidelberg (1997)"},{"key":"18_CR4","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":"18_CR5","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":"18_CR6","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"In 2nd International Workshop on Rewriting Logic and its Applications (WRLA 1998)","author":"F. Dur\u00e1n","year":"1998","unstructured":"Dur\u00e1n, F., Meseguer, J.: An extensible module algebra for Maude. In: In 2nd International Workshop on Rewriting Logic and its Applications (WRLA 1998). Electronic Notes in Theoretical Computer Science, vol.\u00a015. Elsevier, Amsterdam (1998)"},{"key":"18_CR7","unstructured":"Filli\u00e2tre, J.-C.: Design of a proof assistant: Coq version 7 (2000) (unpublished)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Harper, R., Lillibridge, M.: A type-theoretic approach to higher-order modules with sharing. In: POPL 1994 [POP94], pp. 123\u2013137 (1994)","DOI":"10.1145\/174675.176927"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10721959_7","volume-title":"Automated Deduction - CADE-17","author":"F. Kamm\u00fcller","year":"2000","unstructured":"Kamm\u00fcller, F.: Modular reasoning in isabelle. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831. Springer, Heidelberg (2000)"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Manifest types, modules, and separate compilation. In: POPL 1994 [POP94], pp. 109\u2013122 (1994)","DOI":"10.1145\/174675.176926"},{"key":"18_CR11","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for JML\/Java program certification (2003) (submitted)"},{"key":"18_CR12","unstructured":"Owre, S., Shankar, N.: The formal semantics of PVS. Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo Park, CA (August 1997)"},{"key":"18_CR13","unstructured":"Conference Record of the 21st Symposium on Principles of Programming Languages, Portland, Oregon. ACM Press, New York (1994)"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/BF01211084","volume":"9","author":"D. Sannella","year":"1997","unstructured":"Sannella, D., Tarlecki, A.: Essential concepts of algebraic specification and program development. Formal Aspects of Computing\u00a09, 229\u2013269 (1997)","journal-title":"Formal Aspects of Computing"}],"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\/10930755_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T01:30:03Z","timestamp":1552613403000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10930755_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540406648","9783540451303"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/10930755_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}