Locales
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
- 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
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- Mechanically proving determinacy of hierarchical block diagram translations
- From types to sets by local type definition in higher-order logic
- A formalization of the Smith normal form in higher-order logic
- A scalable module system
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- The expressive power of monotonic parallel composition
- Mechanical Verification of a Constructive Proof for FLP
- Eisbach: a proof method language for Isabelle
- Mechanizing a process algebra for network protocols
- The Isabelle Framework
- A graph library for Isabelle
- Local Theory Specifications in Isabelle/Isar
- A formalized general theory of syntax with bindings: extended version
- The adequacy of Launchbury's natural semantics for lazy evaluation
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- A comprehensive framework for saturation theorem proving
- Proving divide and conquer complexities in Isabelle/HOL
- Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths
- Simple type theory is not too simple: Grothendieck's schemes without dependent types
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- Isabelle
- Isabelle/Isar
- Isabelle/jEdit
- CeTA
- HOL-Omega
- CompCertTSO
- STEXIDE
- EasyCrypt
- Autoref
- Eisbach
- pGCL
- ConfiChair
- QuickChick
- CoSMed
- Matrix Operations
- IsaFoL
- SL2SX
- Lifting
- Transfer
- Chapar
- CSimpl
- CoSP
- Tycon
- DPT
- Akra Bazzi
- Coinductive
- Cayley-Hamilton
- CAVA Automata Library
- Archive Formal Proofs
- CAVA
- BicolanoMT
- Berlekamp Zassenhaus
- Completeness theorem
- Arrow Gibbard Satterthwaite
- Edmonds-Karp
- Echelon Form
- Density Compiler
- Jinja Threads
- Jordan Normal Forms
- CAVA LTL Modelchecker
- Constructive Proof FLP
- Monomorphic Monad
- Logtk
- LLL Factorization
- Paraconsistency
- Psi-calculi
- NASA PVS
- Gabow SCC
- Social Choice Theory
- LTL_to_DRA
- Root Balanced Tree
- AWN
- Propositional Resolution
- Nested Multisets
- SAT Solver Verification
- Girth-Chromatic
- Launchbury
- LTL_to_GBA
- Superposition Calculus
- Tame Graphs
- Stone Algebras
- Real_Impl
- Zoo Probabilistic Systems
- Stable Matching
- Verified LLL
- Vector Spaces
- Landau Symbols
- ATOM
- Tree Automata
- Secondary Sylow
- DudeTM
- CLDC
- Mnemosyne
- Call_Arity
- AutoCorres
- Matrix_Tensor
This page was built for software: Locales
