Locales
From MaRDI portal
Software:24376
swMATH12448MaRDI QIDQ24376FDOQ24376
Author name not available (Why is that?)
Cited In (49)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL
- Mechanically proving determinacy of hierarchical block diagram translations
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
- From types to sets by local type definition in higher-order logic
- A formalization of the Smith normal form in higher-order logic
- Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types
- A scalable module system
- CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- Mechanical Verification of a Constructive Proof for FLP
- Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem
- The Isabelle Framework
- Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
- Eisbach: a proof method language for Isabelle
- Mechanizing a process algebra for network protocols
- A Formalisation of Finite Automata Using Hereditarily Finite Sets
- Local Theory Specifications in Isabelle/Isar
- The adequacy of Launchbury's natural semantics for lazy evaluation
- A graph library for Isabelle
- A formalized general theory of syntax with bindings: extended version
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- A comprehensive framework for saturation theorem proving
- The Expressive Power of Monotonic Parallel Composition
- Proving divide and conquer complexities in Isabelle/HOL
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- A verified SAT solver framework with learn, forget, restart, and incrementality
- CoSMed: a confidentiality-verified social media platform
- Introduction to ``Milestones in interactive theorem proving
- Mechanising a type-safe model of multithreaded Java with a verified compiler
- First-Class Type Classes
- Verification and code generation for invariant diagrams in Isabelle
- Certified quantum computation in Isabelle/HOL
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
- Infeasible Paths Elimination by Symbolic Execution Techniques
- A comprehensive framework for saturation theorem proving
- From LCF to Isabelle/HOL
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
- Effect polymorphism in higher-order logic (proof pearl)
- Effect polymorphism in higher-order logic (proof pearl)
- Title not available (Why is that?)
- Locales: a module system for mathematical theories
- Nine Chapters of Analytic Number Theory in Isabelle/HOL.
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Exploring the structure of an algebra text with locales
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- Automatic refinement to efficient data structures: a comparison of two approaches
- Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
This page was built for software: Locales