The following pages link to HOL (Q17631):
Displaying 50 items.
- Evaluating general purpose automated theorem proving systems (Q1606324) (← links)
- On the desirability of mechanizing calculational proofs (Q1607098) (← links)
- Formal analysis of the kinematic Jacobian in screw theory (Q1624599) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Formally verified algorithms for upper-bounding state space diameters (Q1663245) (← links)
- Formal kinematic analysis of a general 6R manipulator using the screw theory (Q1665987) (← links)
- The formalization of discrete Fourier transform in HOL (Q1666338) (← links)
- A theory of formal synthesis via inductive learning (Q1674868) (← links)
- Formalization of fractional order PD control systems in HOL4 (Q1680557) (← links)
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system (Q1687709) (← links)
- How to simulate it in Isabelle: towards formal proof for secure multi-party computation (Q1687724) (← links)
- FoCaLiZe and Dedukti to the rescue for proof interoperability (Q1687726) (← links)
- Proof certificates in PVS (Q1687741) (← links)
- Towards verification of cyber-physical systems with UTP and Isabelle/HOL (Q1708708) (← links)
- Proof pearl: Bounding least common multiples with triangles (Q1722641) (← 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)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- Organizing numerical theories using axiomatic type classes (Q1774558) (← links)
- An algebraic framework for minimum spanning tree problems (Q1786562) (← 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)
- HOL Light QE (Q1791161) (← links)
- ProofWatch: watchlist guidance for large theories in E (Q1791167) (← links)
- Program verification in the presence of cached address translation (Q1791200) (← links)
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (Q1798665) (← 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)
- ATPboost: learning premise selection in binary setting with ATP feedback (Q1799117) (← links)
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions (Q1799129) (← links)
- Structuring and automating hardware proofs in a higher-order theorem- proving environment (Q1801500) (← links)
- Algebraic models of microprocessors architecture and organisation (Q1815999) (← links)
- The foundation of a generic theorem prover (Q1823013) (← links)
- A trustworthy proof checker (Q1826468) (← links)
- Structuring metatheory on inductive definitions (Q1854368) (← links)
- Planning proofs of equations in CCS (Q1857269) (← links)
- Weakest pre-condition reasoning for Java programs with JML annotations (Q1881666) (← links)
- Interpreting HOL in the calculus of constructions (Q1885479) (← links)
- Secure mechanical verification of mutually recursive procedures (Q1887136) (← links)
- Indentification of inductive properties during verification of synchronous sequential circuits (Q1893131) (← links)
- TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker (Q1935352) (← links)
- Unifying theories in ProofPower-Z (Q1941892) (← links)
- Quantified multimodal logics in simple type theory (Q1945702) (← links)
