Locales

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