Locales: a module system for mathematical theories

DOI10.1007/S10817-013-9284-7zbMath1315.68218OpenAlexW2061969020MaRDI QIDQ2352487

Clemens Ballarin

Publication date: 2 July 2015

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-013-9284-7

zbMATH Keywords

module systemIsabelletheorem provertheory hierarchytheory interpretation

Mathematics Subject Classification ID

Related Items (35)

Proving divide and conquer complexities in Isabelle/HOL ⋮ Eisbach: a proof method language for Isabelle ⋮ Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL ⋮ A Formalisation of Finite Automata Using Hereditarily Finite Sets ⋮ Mechanising a type-safe model of multithreaded Java with a verified compiler ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ The adequacy of Launchbury's natural semantics for lazy evaluation ⋮ Certified quantum computation in Isabelle/HOL ⋮ Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Unnamed Item ⋮ A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL ⋮ Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ Exploring the structure of an algebra text with locales ⋮ Unnamed Item ⋮ From types to sets by local type definition in higher-order logic ⋮ Nine Chapters of Analytic Number Theory in Isabelle/HOL. ⋮ A verified implementation of the Berlekamp-Zassenhaus factorization algorithm ⋮ Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL ⋮ A graph library for Isabelle ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ From LCF to Isabelle/HOL ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic ⋮ The Expressive Power of Monotonic Parallel Composition ⋮ A comprehensive framework for saturation theorem proving ⋮ Distilling the requirements of Gödel's incompleteness theorems with a proof assistant ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ Infeasible Paths Elimination by Symbolic Execution Techniques ⋮ A comprehensive framework for saturation theorem proving ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory ⋮ A formalization of the Smith normal form in higher-order logic

Uses Software

• AXIOM
• Coq
• Isabelle
• Isabelle/Isar
• Scala
• Locales
• MathScheme

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
• Constructive Type Classes in Isabelle
• Local Theory Specifications in Isabelle/Isar
• A theory of mixin modules: basic and derived operators
• Types for Proofs and Programs
• Interpretation of Locales in Isabelle: Theories and Proof Contexts

This page was built for publication: Locales: a module system for mathematical theories