Locales
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Isabelle
- Isabelle/Isar
- 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
- From types to sets by local type definition in higher-order logic
- Isabelle/jEdit
- HOL-Omega
- CeTA
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- STEXIDE
- 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
- A graph library for Isabelle
- CompCertTSO
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- 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
- EasyCrypt
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- Exploring the structure of an algebra text with locales
- From LCF to Isabelle/HOL
- Mechanically proving determinacy of hierarchical block diagram translations
- Locales: a module system for mathematical theories
- Proving divide and conquer complexities in Isabelle/HOL
- Automatic refinement to efficient data structures: a comparison of two approaches
- Autoref
- Eisbach
- pGCL
- ConfiChair
- QuickChick
- Certified quantum computation in Isabelle/HOL
- Probabilistic functions and cryptographic oracles in higher order logic
- The expressive power of monotonic parallel composition
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths
- Mechanical Verification of a Constructive Proof for FLP
- Eisbach: a proof method language for Isabelle
- Mechanizing a process algebra for network protocols
- Proof pearl: a probabilistic proof for the girth-chromatic number theorem
- CoSMed
- Verified efficient enumeration of plane graphs modulo isomorphism
- IsaFoL
- SL2SX
- Transfer
- Lifting
- CSimpl: a rely-guarantee-based framework for verifying concurrent programs
- Chapar
- CSimpl
- A formalisation of finite automata using hereditarily finite sets
- The Isabelle Framework
- First-Class Type Classes
- Local Theory Specifications in Isabelle/Isar
- Tycon
- CoSP
- A scalable module system
- DPT
- Coinductive
- Jinja Threads
- Zoo Probabilistic Systems
- Edmonds-Karp
- Echelon Form
- Completeness theorem
- Cayley-Hamilton
- Jordan Normal Forms
- CAVA Automata Library
- CAVA
- Superposition Calculus
- Paraconsistency
- Psi-calculi
- Tame Graphs
- Monomorphic Monad
- BicolanoMT
- Akra Bazzi
- Berlekamp Zassenhaus
- Stone Algebras
- Social Choice Theory
- Archive Formal Proofs
- Logtk
- Stable Matching
- Arrow Gibbard Satterthwaite
- NASA PVS
- Root Balanced Tree
- Density Compiler
- LLL Factorization
- Verified LLL
- Vector Spaces
- Matrix Operations
- LTL_to_DRA
- CAVA LTL Modelchecker
- SAT Solver Verification
- Constructive Proof FLP
- Tree Automata
- Propositional Resolution
- Nested Multisets
- Gabow SCC
- AWN
- LTL_to_GBA
This page was built for software: Locales
