Locales
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).
Keywords for this software
References in zbMATH (referenced in 39 articles )
Showing results 1 to 20 of 39.
Sorted by year (- Ballarin, Clemens: Exploring the structure of an algebra text with locales (2020)
- Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (2020)
- Echenim, Mnacho; Guiol, Hervé; Peltier, Nicolas: Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL (2020)
- Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
- Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2020)
- Thiemann, René; Bottesch, Ralph; Divasón, Jose; Haslbeck, Max W.; Joosten, Sebastiaan J. C.; Yamada, Akihisa: Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (2020)
- Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
- Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
- Lochbihler, Andreas: Effect polymorphism in higher-order logic (proof pearl) (2019)
- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
- Preoteasa, Viorel; Dragomir, Iulia; Tripakis, Stavros: Mechanically proving determinacy of hierarchical block diagram translations (2019)
- Avigad, Jeremy (ed.); Blanchette, Jasmin Christian (ed.); Klein, Gerwin (ed.); Paulson, Lawrence (ed.); Popescu, Andrei (ed.); Snelting, Gregor (ed.): Introduction to “Milestones in interactive theorem proving” (2018)
- Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)
- Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
- Breitner, Joachim: The adequacy of Launchbury’s natural semantics for lazy evaluation (2018)
- Lochbihler, Andreas: Mechanising a type-safe model of multithreaded Java with a verified compiler (2018)
- Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2018)
- Eberl, Manuel: Proving divide and conquer complexities in Isabelle/HOL (2017)
- Lochbihler, Andreas: Effect polymorphism in higher-order logic (proof pearl) (2017)
- Sanán, David; Zhao, Yongwang; Hou, Zhe; Zhang, Fuyuan; Tiu, Alwen; Liu, Yang: CSimpl: a rely-guarantee-based framework for verifying concurrent programs (2017)