Locales: a module system for mathematical theories
From MaRDI portal
Publication:2352487
DOI10.1007/s10817-013-9284-7zbMath1315.68218OpenAlexW2061969020MaRDI QIDQ2352487
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
Related Items
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
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
