swMATH12448MaRDI QIDQ24376FDOQ24376
Author name not available (Why is that?)
Official website: http://link.springer.com/article/10.1007%2Fs10817-013-9284-7
Cited In (only showing first 100 items - show all)
- A scalable module system
- Mechanical Verification of a Constructive Proof for FLP
- The Isabelle Framework
- Eisbach: a proof method language for Isabelle
- Mechanizing a process algebra for network protocols
- 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
- Program-Conflict-Analysis
- Naiad
- Sqrt_Babylonian
- Verification and code generation for invariant diagrams in Isabelle
- GraphQL
- FlowFox
- Boolean_Expression_Checkers
- MFMC_Countable
- Jacobson_Basic_Algebra
- Ordered_Resolution_Prover
- Saturation_Framework
- CoCon
- Effect polymorphism in higher-order logic (proof pearl)
- Locales: a module system for mathematical theories
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Proof pearl: a probabilistic proof for the girth-chromatic number theorem
- A formalisation of finite automata using hereditarily finite sets
- 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
This page was built for software: Locales
