Locales

No author found.

Related Items (49)

Proving divide and conquer complexities in Isabelle/HOL ⋮ Eisbach: a proof method language for Isabelle ⋮ Mechanizing a process algebra for network protocols ⋮ Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL ⋮ A Formalisation of Finite Automata Using Hereditarily Finite Sets ⋮ Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem ⋮ Introduction to ``Milestones in interactive theorem proving ⋮ CoSMed: a confidentiality-verified social media platform ⋮ 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 ⋮ A scalable module system ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ Unnamed Item ⋮ Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ Exploring the structure of an algebra text with locales ⋮ A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L ⋮ From types to sets by local type definition in higher-order logic ⋮ The Isabelle Framework ⋮ First-Class Type Classes ⋮ Verification and code generation for invariant diagrams in Isabelle ⋮ Nine Chapters of Analytic Number Theory in Isabelle/HOL. ⋮ CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs ⋮ A formalized general theory of syntax with bindings: extended version ⋮ A verified implementation of the Berlekamp-Zassenhaus factorization algorithm ⋮ Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL ⋮ Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs ⋮ A graph library for Isabelle ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ From LCF to Isabelle/HOL ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Mechanically proving determinacy of hierarchical block diagram translations ⋮ 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 ⋮ Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism ⋮ Local Theory Specifications in Isabelle/Isar ⋮ Infeasible Paths Elimination by Symbolic Execution Techniques ⋮ Mechanical Verification of a Constructive Proof for FLP ⋮ 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 ⋮ Locales: a module system for mathematical theories

This page was built for software: Locales