The following pages link to Locales (Q24376):
Displayed 49 items.
- Eisbach: a proof method language for Isabelle (Q287365) (← links)
- Mechanizing a process algebra for network protocols (Q287372) (← links)
- A scalable module system (Q391632) (← links)
- Verification and code generation for invariant diagrams in Isabelle (Q478381) (← links)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
- Mechanising a type-safe model of multithreaded Java with a verified compiler (Q1663233) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- From types to sets by local type definition in higher-order logic (Q1722645) (← links)
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L (Q1961914) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (Q1984794) (← links)
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL (Q1984795) (← links)
- A graph library for Isabelle (Q2018659) (← links)
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory (Q2102926) (← links)
- A formalization of the Smith normal form in higher-order logic (Q2102950) (← links)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (Q2209537) (← links)
- Exploring the structure of an algebra text with locales (Q2209550) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Mechanically proving determinacy of hierarchical block diagram translations (Q2287118) (← links)
- Locales: a module system for mathematical theories (Q2352487) (← links)
- Proving divide and conquer complexities in Isabelle/HOL (Q2362108) (← links)
- Automatic refinement to efficient data structures: a comparison of two approaches (Q2417948) (← links)
- Certified quantum computation in Isabelle/HOL (Q2666954) (← links)
- Probabilistic Functions and Cryptographic Oracles in Higher Order Logic (Q2802495) (← links)
- The Expressive Power of Monotonic Parallel Composition (Q2802500) (← links)
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
- Infeasible Paths Elimination by Symbolic Execution Techniques (Q2829242) (← links)
- Mechanical Verification of a Constructive Proof for FLP (Q2829253) (← links)
- Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem (Q2914757) (← links)
- Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism (Q3088012) (← links)
- CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs (Q3303910) (← links)
- A Formalisation of Finite Automata Using Hereditarily Finite Sets (Q3454094) (← links)
- The Isabelle Framework (Q3543647) (← links)
- First-Class Type Classes (Q3543665) (← links)
- Local Theory Specifications in Isabelle/Isar (Q3638251) (← links)
- The adequacy of Launchbury's natural semantics for lazy evaluation (Q4577822) (← links)
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL (Q5049005) (← links)
- Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types (Q5094472) (← links)
- Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs (Q5170835) (← links)
- (Q5875419) (← links)
- Nine Chapters of Analytic Number Theory in Isabelle/HOL. (Q5875424) (← links)
- Effect polymorphism in higher-order logic (proof pearl) (Q5915785) (← links)
- Formalizing Bachmair and Ganzinger's ordered resolution prover (Q5916290) (← links)
- A comprehensive framework for saturation theorem proving (Q5918558) (← links)
- Formalizing Bachmair and Ganzinger's ordered resolution prover (Q5919011) (← links)
- Effect polymorphism in higher-order logic (proof pearl) (Q5919584) (← links)
- A comprehensive framework for saturation theorem proving (Q5970776) (← links)