Locales swMATH ID: 12448 Software Authors: Ballarin, Clemens Description: Locales: a module system for mathematical theories. Locales are a module system for managing theory hierarchies in a theorem prover through theory interpretation. They are available for the theorem prover Isabelle. In this paper, their semantics is defined in terms of local theories and morphisms. Locales aim at providing flexible means of extension and reuse. Theory modules (which are called locales) may be extended by definitions and theorems. Interpretation to Isabelle’s global theories and proof contexts is possible via morphisms. Even the locale hierarchy may be changed if declared relations between locales do not adequately reflect logical relations, which are implied by the locales’ specifications. By discussing their design and relating it to more commonly known structuring mechanisms of programming languages and provers, locales are made accessible to a wider audience beyond the users of Isabelle. The discussed mechanisms include ML-style functors, type classes and mixins (the latter are found in modern object-oriented languages). Homepage: http://link.springer.com/article/10.1007%2Fs10817-013-9284-7 Dependencies: Isabelle Keywords: theorem prover; module system; theory hierarchy; theory interpretation; Isabelle Related Software: Isabelle/HOL; Isabelle; HOL; Archive Formal Proofs; Coq; Sledgehammer; Isar; Isabelle/Isar; CeTA; seL4; Lifting; Transfer; Mizar; Flyspeck; Nominal Isabelle; HOL Light; AVATAR; Isabelle/jEdit; VAMPIRE; ML Cited in: 42 Publications all top 5 Cited by 74 Authors 6 Paulson, Lawrence Charles 5 Blanchette, Jasmin Christian 5 Lochbihler, Andreas 4 Popescu, Andrei 4 Wenzel, Makarius 3 Nipkow, Tobias 3 Thiemann, René 3 Traytel, Dmitry 2 Ballarin, Clemens 2 Bordg, Anthony 2 Divasón, Jose 2 Fleury, Mathias 2 Joosten, Sebastiaan J. C. 2 Lammich, Peter 2 Noschinski, Lars 2 Preoteasa, Viorel 2 Schlichtkrull, Anders 2 Waldmann, Uwe 2 Weidenbach, Christoph 2 Yamada, Akihisa 1 Aissat, Romain 1 Åman Pohjola, Johannes 1 Avigad, Jeremy 1 Back, Ralph-Johan 1 Bauereiß, Thomas 1 Bisping, Benjamin 1 Bottesch, Ralph Christian 1 Bourke, Timothy 1 Breitner, Joachim 1 Brodmann, Paul-David 1 Dragomir, Iulia 1 Eberl, Manuel 1 Echenim, Mnacho 1 Eriksson, Johannes 1 Gheri, Lorenzo 1 Guiol, Hervé 1 Haftmann, Florian 1 Haslbeck, Max W. 1 He, Yijun 1 Höfner, Peter 1 Hou, Zhe 1 Jungnickel, Tim 1 Kammüller, Florian 1 Klein, Gerwin 1 Kohlhase, Michael 1 Kunčar, Ondřej 1 Lachnitt, Hanna 1 Li, Wenda 1 Liu, Yang 1 Matichuk, Daniel 1 Murray, Toby 1 Nestmann, Uwe 1 Oury, Nicolas 1 Parrow, Joachim 1 Peltier, Nicolas 1 Pesenti Gritti, Armando 1 Peters, Kirstin 1 Rabe, Florian 1 Raimondi, Franco 1 Rickmann, Christina 1 Sanán, David 1 Seidler, Henning 1 Snelting, Gregor 1 Sozeau, Matthieu 1 Sternagel, Christian 1 Stüber, Anke 1 Tiu, Alwen Fernanto 1 Tripakis, Stavros 1 van Glabbeek, Robert Jan 1 Voisin, Frédéric 1 Wilhelm-Weidner, Arno 1 Wolff, Burkhart 1 Zhang, Fuyuan 1 Zhao, Yongwang all top 5 Cited in 7 Serials 20 Journal of Automated Reasoning 1 Information and Computation 1 Formal Aspects of Computing 1 Experimental Mathematics 1 Journal of Functional Programming 1 Mathematics in Computer Science 1 Journal of Logical and Algebraic Methods in Programming all top 5 Cited in 13 Fields 41 Computer science (68-XX) 7 Mathematical logic and foundations (03-XX) 3 Combinatorics (05-XX) 2 Number theory (11-XX) 1 General and overarching topics; collections (00-XX) 1 Field theory and polynomials (12-XX) 1 Commutative algebra (13-XX) 1 Algebraic geometry (14-XX) 1 Group theory and generalizations (20-XX) 1 Convex and discrete geometry (52-XX) 1 Quantum theory (81-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year