{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T05:13:25Z","timestamp":1740287605012,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642141270"},{"type":"electronic","value":"9783642141287"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14128-7_32","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T10:45:36Z","timestamp":1277808336000},"page":"370-384","source":"Crossref","is-referenced-by-count":8,"title":["Towards MKM in the Large: Modular Representation and Scalable Software Architecture"],"prefix":"10.1007","author":[{"given":"Michael","family":"Kohlhase","sequence":"first","affiliation":[]},{"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[]},{"given":"Vyacheslav","family":"Zholudev","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-3-540-44616-3_5","volume-title":"Recent Trends in Algebraic Development Techniques","author":"S. Autexier","year":"2000","unstructured":"Autexier, S., Hutter, D., Mantel, H., Schairer, A.: Towards an Evolutionary Formal Software-Development Using CASL. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol.\u00a01827, pp. 73\u201388. Springer, Heidelberg (2000)"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Berners-Lee, T., Fielding, R., Masinter, L.: Uniform Resource Identifier (URI): Generic Syntax, RFC 3986, Internet Engineering Task Force (2005)","DOI":"10.17487\/rfc3986"},{"key":"32_CR3","volume-title":"Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"32_CR4","volume-title":"Elements of Mathematics","author":"N. Bourbaki","year":"1968","unstructured":"Bourbaki, N.: Theory of Sets. In: Elements of Mathematics, Springer, Heidelberg (1968)"},{"key":"32_CR5","volume-title":"Elements of Mathematics","author":"N. Bourbaki","year":"1974","unstructured":"Bourbaki, N.: Algebra I. In: Elements of Mathematics, Springer, Heidelberg (1974)"},{"key":"32_CR6","unstructured":"Buswell, S., Caprotti, O., Carlisle, D., Dewar, M., Gaetano, M., Kohlhase, M.: The Open Math Standard, Version 2.0. Technical report, The Open Math Society (2004), http:\/\/www.openmath.org\/standard\/om20"},{"key":"32_CR7","unstructured":"CoFI, The Common Framework Initiative. In: CASL Reference Manual. LNCS, vol.\u00a02960. Springer, Heidelberg (2004)"},{"key":"32_CR8","volume-title":"Combinatory Logic","author":"H. Curry","year":"1958","unstructured":"Curry, H., Feys, R.: Combinatory Logic. North-Holland, Amsterdam (1958)"},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"Dumbrava, S., Horozal, F., Sojakova, K.: A Case Study on Formalizing Algebra in a Module System. In: Rabe, F., Sch\u00fcrmann, C. (eds.) Workshop on Modules and Libraries for Proof Assistants. ACM International Conference Proceeding Series, vol.\u00a0429, pp. 11\u201318 (2009)","DOI":"10.1145\/1735813.1735816"},{"key":"32_CR10","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/10721959_8","volume-title":"Conference on Automated Deduction","author":"W. Farmer","year":"2000","unstructured":"Farmer, W.: An Infrastructure for Intertheory Reasoning. In: McAllester, D. (ed.) Conference on Automated Deduction, pp. 115\u2013131. Springer, Heidelberg (2000)"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"Farmer, W., Guttman, J., Thayer, F.: Little Theories. In: Kapur, D. (ed.) Conference on Automated Deduction, pp. 467\u2013581 (1992)","DOI":"10.1007\/3-540-55602-8_192"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Farmer, W.M.: Mathematical Knowledge Management. In: Schwartz, D.G. (ed.) Mathematical Knowledge Management, pp. 599\u2013604. Idea Group Reference (2005)","DOI":"10.4018\/978-1-59140-573-3.ch078"},{"key":"32_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-02614-0_24","volume-title":"Intelligent Computer Mathematics","author":"J. Giceva","year":"2009","unstructured":"Giceva, J., Lange, C., Rabe, F.: Integrating Web Services into Active Mathematical Documents. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) Calculemus 2009. LNCS, vol.\u00a05625, pp. 279\u2013293. Springer, Heidelberg (2009)"},{"key":"32_CR14","unstructured":"Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.: Introducing OBJ. In: Goguen, J., Coleman, D., Gallimore, R. (eds.) Applications of Algebraic Specification using OBJ, Cambridge (1993)"},{"key":"32_CR15","doi-asserted-by":"crossref","unstructured":"Horozal, F., Rabe, F.: Representing Model Theory in a Type-Theoretical Logical Framework. In: Fourth Workshop on Logical and Semantic Frameworks, with Applications. Electronic Notes in Theoretical Computer Science, vol.\u00a0256, pp. 49\u201365 (2009)","DOI":"10.1016\/j.entcs.2009.11.005"},{"key":"32_CR16","unstructured":"Horozal, F., Rabe, F.: Representing Model Theory in a Type-Theoretical Logical Framework. Under review (2010), http:\/\/kwarc.info\/frabe\/Research\/EArabe_folsound_10.pdf"},{"key":"32_CR17","first-page":"479","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism","author":"W. Howard","year":"1980","unstructured":"Howard, W.: The formulas-as-types notion of construction. In: To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pp. 479\u2013490. Academic Press, London (1980)"},{"key":"32_CR18","unstructured":"Kohlhase, M., Mossakowski, T., Rabe, F.: The LATIN Project (2009), https:\/\/trac.omdoc.org\/LATIN\/"},{"key":"32_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-540-85110-3_41","volume-title":"Intelligent Computer Mathematics","author":"M. Kohlhase","year":"2008","unstructured":"Kohlhase, M., M\u00fcller, C., Rabe, F.: Notations for Living Mathematical Documents. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS (LNAI), vol.\u00a05144, pp. 504\u2013519. Springer, Heidelberg (2008)"},{"key":"32_CR20","unstructured":"Kohlhase, M., Rabe, F., Sacerdoti Coen, C.: A Foundational View on Integration Problems (2010) (Submitted to CALCULEMUS)"},{"key":"32_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-71209-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Mossakowski","year":"2007","unstructured":"Mossakowski, T., Maeder, C., L\u00fcttich, K.: The Heterogeneous Tool Set. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 519\u2013522. Springer, Heidelberg (2007)"},{"key":"32_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/3-540-44755-5_23","volume-title":"Theorem Proving in Higher Order Logics","author":"P. Naumov","year":"2001","unstructured":"Naumov, P., Stehr, M., Meseguer, J.: The HOL\/NuPRL proof translator - a practical approach to formal interoperability. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, p. 329. Springer, Heidelberg (2001)"},{"key":"32_CR23","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"32_CR24","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala. artima (2007)"},{"key":"32_CR25","first-page":"748","volume-title":"11th International Conference on Automated Deduction (CADE)","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) 11th International Conference on Automated Deduction (CADE), pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"32_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"32_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"32_CR28","unstructured":"Poswolsky, A., Sch\u00fcrmann, C.: System Description: Delphin - A Functional Programming Language for Deductive Systems. In: Abel, A., Urban, C. (eds.) International Workshop on Logical Frameworks and Metalanguages: Theory and Practice. ENTCS, pp. 135\u2013141 (2008)"},{"key":"32_CR29","unstructured":"Rabe, F.: Representing Logics and Logic Translations. PhD thesis, Jacobs University Bremen (2008), http:\/\/kwarc.info\/frabe\/Research\/phdthesis.pdf"},{"key":"32_CR30","unstructured":"Rabe, F.: The MMT System (2008), https:\/\/trac.kwarc.info\/MMT\/"},{"key":"32_CR31","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1577824.1577831","volume-title":"Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP)","author":"F. Rabe","year":"2009","unstructured":"Rabe, F., Sch\u00fcrmann, C.: A Practical Module System for LF. In: Cheney, J., Felty, A. (eds.) Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), pp. 40\u201348. ACM Press, New York (2009)"},{"key":"32_CR32","first-page":"413","volume-title":"Fundamentals of Computation Theory","author":"D. Sannella","year":"1983","unstructured":"Sannella, D., Wirsing, M.: A Kernel Language for Algebraic Specification and Implementation. In: Karpinski, M. (ed.) Fundamentals of Computation Theory, pp. 413\u2013427. Springer, Heidelberg (1983)"},{"key":"32_CR33","unstructured":"Trybulec, A., Blair, H.: Computer Assisted Reasoning with MIZAR. In: Joshi, A. (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp. 26\u201328 (1985)"},{"key":"32_CR34","doi-asserted-by":"crossref","unstructured":"Zholudev, V., Kohlhase, M.: TNTBase: a Versioned Storage for XML. In: Proceedings of Balisage: The Markup Conference 2009, vol.\u00a03, Mulberry Technologies, Inc. (2009)","DOI":"10.4242\/BalisageVol3.Zholudev01"},{"key":"32_CR35","unstructured":"Zholudev, V., Kohlhase, M., Rabe, F.: A (insert XML Format) Database for (insert cool application). In: Proceedings of XMLPrague, XMPPrague.cz (2010)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14128-7_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T09:24:23Z","timestamp":1740216263000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14128-7_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141270","9783642141287"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14128-7_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}