{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T17:16:52Z","timestamp":1771262212542,"version":"3.50.1"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,4,10]],"date-time":"2013-04-10T00:00:00Z","timestamp":1365552000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,2]]},"DOI":"10.1007\/s10817-013-9284-7","type":"journal-article","created":{"date-parts":[[2013,4,9]],"date-time":"2013-04-09T01:23:21Z","timestamp":1365470601000},"page":"123-153","source":"Crossref","is-referenced-by-count":71,"title":["Locales: A Module System for Mathematical Theories"],"prefix":"10.1007","volume":"52","author":[{"given":"Clemens","family":"Ballarin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,4,10]]},"reference":[{"key":"9284_CR1","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1017\/S0960129598002576","volume":"8","author":"D Ancona","year":"1998","unstructured":"Ancona, D., Zucca, E.: A theory of mixin modules: basic and derived operators. Math. Struct. Comput. Sci. 8, 401\u2013446 (1998)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9284_CR2","doi-asserted-by":"crossref","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) Types for Proofs and Programs, TYPES 2003, Torino, Italy. LNCS 3085, pp.\u00a034\u201350. Springer (2004)","DOI":"10.1007\/978-3-540-24849-1_3"},{"key":"9284_CR3","unstructured":"Ballarin, C.: Interpretation of locales in Isabelle: managing dependencies between locales. Tech. Rep. TUM-I0607, Technische Universit\u00e4t M\u00fcnchen (2006)"},{"key":"9284_CR4","doi-asserted-by":"crossref","unstructured":"Ballarin, C.: Interpretation of locales in Isabelle: theories and proof contexts. In: Borwein, J.M., Farmer, W.M. (eds.) Mathematical Knowledge Management, MKM 2006, Wokingham, UK. LNCS 4108, pp. 31\u201343. Springer (2006)","DOI":"10.1007\/11812289_4"},{"key":"9284_CR5","unstructured":"Ballarin, C.: Tutorial to locales and locale interpretation. In: Lamb\u00e1n, L., Romero, A., Rubio,\u00a0J. (eds.) Contribuciones Cient\u00edficas en Honor de Mirian Andr\u00e9s G\u00f3mez. Servicio de Publicaciones de la Universidad de La Rioja, Logro\u00f1o, Spain (2010). Also part of the Isabelle user documentation"},{"key":"9284_CR6","unstructured":"Bracha, G.: The programming language Jigsaw: mixins, modulariy and multiple inheritance. Ph.D. thesis, University of Utah (1992). Also Technical Report UUCS-92-007"},{"key":"9284_CR7","unstructured":"Carette, J., Farmer, W.M., Jeremic, F., Maccio, V., O\u2019Connor, R., Tran, Q.M.: The MathScheme library: some preliminary experiments. Manuscript arXiv:1106.1862v1 (2011)"},{"key":"9284_CR8","doi-asserted-by":"crossref","unstructured":"Farmer, W.M., Guttman, J.D., Thayer, F.J.: Little theories. In: Kapur, D. (ed.) Automated deduction, CADE-11: Saratoga Springs, NY, USA. LNCS 607, pp. 567\u2013581. Springer-Verlag (1992)","DOI":"10.1007\/3-540-55602-8_192"},{"key":"9284_CR9","unstructured":"Gunter, E.L.: Doing algebra in simple type theory. Tech. Rep. MS-CIS-89-38, University of Pennsylvania (1989)"},{"key":"9284_CR10","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) Types for Proofs and Programs, TYPES 2006, Nottingham, UK. LNCS\u00a04502, pp. 160\u2013174. Springer (2007). doi: 10.1007\/978-3-540-74464-1_11","DOI":"10.1007\/978-3-540-74464-1_11"},{"key":"9284_CR11","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Wenzel, M.: Local theory specifications in Isabelle\/Isar. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) Types for Proofs and Programs, TYPES 2008, Torino, Italy. LNCS\u00a05497, pp. 153\u2013168. Springer (2009). doi: 10.1007\/978-3-642-02444-3_10","DOI":"10.1007\/978-3-642-02444-3_10"},{"key":"9284_CR12","unstructured":"Harper, R., Pierce, B.C.: Design considerations for ML-style module systems. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages. MIT Press (2005)"},{"key":"9284_CR13","doi-asserted-by":"crossref","unstructured":"Jenks, R.D., Sutor, R.S.: AXIOM: The Scientific Computation System. Springer-Verlag (1992)","DOI":"10.1007\/978-1-4612-2940-7"},{"key":"9284_CR14","unstructured":"Kamm\u00fcller, F.: Modular reasoning in Isabelle. Ph.D. thesis, University of Cambridge, Computer Laboratory (1999). Also Technical Report No. 470"},{"key":"9284_CR15","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales: a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) Theorem Proving in Higher Order Logics: TPHOLs\u201999, Nice, France. LNCS 1690, pp. 149\u2013165. Springer (1999)","DOI":"10.1007\/3-540-48256-3_11"},{"key":"9284_CR16","unstructured":"Milner, R., Tofte, M.: Commentary on Standard ML. MIT Press, Cambridge (1990)"},{"key":"9284_CR17","first-page":"164","volume-title":"Logical Environments","author":"T Nipkow","year":"1993","unstructured":"Nipkow, T.: Order-sorted polymorphism in Isabelle. In: Huet, G., Plotkin, G. (eds.) Logical Environments, pp. 164\u2013188. Cambridge University Press, Cambridge (1993)"},{"key":"9284_CR18","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Verified efficient enumeration of plane graphs modulo isomorphism. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving (ITP 2011). LNCS 6898, pp. 281\u2013296. Springer (2011)","DOI":"10.1007\/978-3-642-22863-6_21"},{"key":"9284_CR19","unstructured":"Odersky, M., Altherr, P., Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E., Zenger, M.: An overview of the Scala programming language. Tech. Rep. IC\/2004\/64, \u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne (2004)"},{"key":"9284_CR20","unstructured":"Java platform, standard edition 6 API specification. http:\/\/docs.oracle.com\/javase\/6\/docs\/api\/ (2011)"},{"key":"9284_CR21","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: The reflection theorem: a study in meta-theoretic reasoning. In: Voronkov, A. (ed.) Automated Deduction\u2014CADE-18 International Conference. LNCS\u00a02392, pp. 377\u2013391. Springer (2002)","DOI":"10.1007\/3-540-45620-1_31"},{"key":"9284_CR22","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/j.entcs.2009.09.065","volume":"254","author":"N Schirmer","year":"2009","unstructured":"Schirmer, N., Wenzel, M.: State spaces\u2014the locale way. Electr. Notes Theor. Comput. Sci. 254, 161\u2013179 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9284_CR23","unstructured":"Soubiran, E.: Modular development of theories and name-space management for the Coq proof assistant. Ph.D. thesis, \u00c9cole Polytechnique (2012)"},{"key":"9284_CR24","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Theorem Proving in Higher Order Logics. LNCS 1275, pp. 307\u2013322 (1997). doi: 10.1007\/BFb0028402","DOI":"10.1007\/BFb0028402"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9284-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9284-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9284-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,25]],"date-time":"2020-07-25T02:40:23Z","timestamp":1595644823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9284-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,10]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["9284"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9284-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,4,10]]}}}