Pages that link to "Item:Q2352487"
From MaRDI portal
The following pages link to Locales: a module system for mathematical theories (Q2352487):
Displaying 39 items.
- Eisbach: a proof method language for Isabelle (Q287365) (← 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 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)
- 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)
- A Formalisation of Finite Automata Using Hereditarily Finite Sets (Q3454094) (← 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)
- Types for Proofs and Programs (Q5712320) (← links)
- (Q5875419) (← links)
- Nine Chapters of Analytic Number Theory in Isabelle/HOL. (Q5875424) (← links)
- Effect polymorphism in higher-order logic (proof pearl) (Q5915785) (← 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)
- (Q6079227) (← links)
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting (Q6108811) (← links)
- Rensets and renaming-based recursion for syntax with bindings extended version (Q6111524) (← links)
- A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL (Q6190081) (← links)
- Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL (Q6611963) (← links)
- Formalizing Coppersmith's method in Isabelle/HOL (Q6648162) (← links)
- Single-set cubical categories and their formalisation with a proof assistant (Q6653090) (← links)