The following pages link to Isabelle/HOL (Q14275):
Displaying 50 items.
- Unifying theories of time with generalised reactive processes (Q1708268) (← links)
- Towards verification of cyber-physical systems with UTP and Isabelle/HOL (Q1708708) (← links)
- Formal proof of a machine closed theorem in Coq (Q1714805) (← links)
- The flow of ODEs: formalization of variational equation and Poincaré map (Q1722644) (← links)
- From types to sets by local type definition in higher-order logic (Q1722645) (← links)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (Q1722647) (← links)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844) (← links)
- Refinement to imperative HOL (Q1739909) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- Completeness in PVS of a nominal unification algorithm (Q1744405) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols (Q1744440) (← links)
- Organizing numerical theories using axiomatic type classes (Q1774558) (← links)
- Relation algebra as programming language using the Ampersand compiler (Q1785856) (← links)
- An algebraic framework for minimum spanning tree problems (Q1786562) (← links)
- An abstract model for proving safety of autonomous urban traffic (Q1786569) (← links)
- Physical addressing on real hardware in Isabelle/HOL (Q1791136) (← links)
- Formalizing ring theory in PVS (Q1791143) (← links)
- Software tool support for modular reasoning in modal logics of actions (Q1791146) (← links)
- Backwards and forwards with separation logic (Q1791147) (← links)
- Tactics and certificates in Meta Dedukti (Q1791152) (← links)
- A formalization of the LLL basis reduction algorithm (Q1791154) (← links)
- A formal proof of the minor-exclusion property for treewidth-two graphs (Q1791156) (← links)
- ProofWatch: watchlist guidance for large theories in E (Q1791167) (← links)
- Verifying the LTL to Büchi automata translation via very weak alternating automata (Q1791171) (← links)
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) (Q1791178) (← links)
- Fast machine words in Isabelle/HOL (Q1791180) (← links)
- Relational parametricity and quotient preservation for modular (co)datatypes (Q1791181) (← links)
- Towards verified handwritten calculational proofs (short paper) (Q1791183) (← links)
- A formally verified solver for homogeneous linear Diophantine equations (Q1791187) (← links)
- Boosting the reuse of formal specifications (Q1791193) (← links)
- Towards formal foundations for game theory (Q1791194) (← links)
- Program verification in the presence of cached address translation (Q1791200) (← links)
- Verified tail bounds for randomized programs (Q1791202) (← links)
- Verified memoization and dynamic programming (Q1791205) (← links)
- \(\mathrm{MDP + TA = PTA}\): probabilistic timed automata, formalized (short paper) (Q1791206) (← links)
- Formalization of a polymorphic subtyping algorithm (Q1791209) (← links)
- Tarski geometry axioms. III (Q1795563) (← links)
- Klein-Beltrami model. I (Q1796767) (← links)
- Klein-Beltrami model. II (Q1796768) (← links)
- Fubini's theorem for non-negative or non-positive functions (Q1796769) (← links)
- Using the Isabelle ontology framework -- linking the formal with the informal (Q1798941) (← links)
- Concrete semantics with Coq and CoqHammer (Q1798946) (← links)
- Isabelle import infrastructure for the Mizar Mathematical Library (Q1798961) (← links)
- Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL (Q1798967) (← links)
- Goal-oriented conjecturing for Isabelle/HOL (Q1798971) (← links)
- Superposition for \(\lambda\)-free higher-order logic (Q1799065) (← links)
- The higher-order prover Leo-III (Q1799072) (← links)
- Superposition with datatypes and codatatypes (Q1799098) (← links)
- Verifying asymptotic time complexity of imperative programs in Isabelle (Q1799114) (← links)
- ATPboost: learning premise selection in binary setting with ATP feedback (Q1799117) (← links)
