The following pages link to Isabelle/HOL (Q14275):
Displaying 50 items.
- External and internal syntax of the \(\lambda \)-calculus (Q968531) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- The axiomatization of override and update (Q975885) (← links)
- A revision of the proof of the Kepler conjecture (Q977177) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- On the correctness of upper layers of automotive systems (Q1019015) (← links)
- Operating system verification---an overview (Q1040002) (← links)
- Winskel is (almost) right: Towards a mechanized semantics textbook (Q1272764) (← links)
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936) (← links)
- Verified bytecode subroutines (Q1405993) (← links)
- Bytecode verification by model checking (Q1405996) (← links)
- Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings (Q1578436) (← links)
- More Church-Rosser proofs (in Isabelle/HOL) (Q1595924) (← links)
- Isabelle/HOL. A proof assistant for higher-order logic (Q1600086) (← links)
- Verifying hybrid systems with modal Kleene algebra (Q1617825) (← links)
- A set solver for finite set relation algebra (Q1617837) (← links)
- Layer systems for confluence -- formalized (Q1623131) (← links)
- How testing helps to diagnose proof failures (Q1624590) (← links)
- Tests and proofs for custom data generators (Q1624592) (← links)
- Formal analysis of the kinematic Jacobian in screw theory (Q1624599) (← links)
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (Q1640636) (← links)
- Nominal unification with atom-variables (Q1640638) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Program extraction for mutable arrays (Q1648867) (← links)
- Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings (Q1653699) (← links)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation (Q1663216) (← links)
- A verified ODE solver and the Lorenz attractor (Q1663218) (← links)
- CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
- Verified iptables firewall analysis and verification (Q1663231) (← links)
- Mechanising a type-safe model of multithreaded Java with a verified compiler (Q1663233) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- A deontic logic reasoning infrastructure (Q1670720) (← links)
- Mechanized proofs of opacity: a comparison of two techniques (Q1673658) (← links)
- A formal proof generator from semi-formal proof documents (Q1675786) (← links)
- Foundational (co)datatypes and (co)recursion for higher-order logic (Q1687535) (← 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)
- Bellerophon: tactical theorem proving for hybrid systems (Q1687737) (← links)
- Efficient, verified checking of propositional proofs (Q1687744) (← links)
- Proof tactics for assertions in separation logic (Q1687747) (← links)
- Gauge integral (Q1688749) (← links)
- Reasoning about algebraic data types with abstractions (Q1694026) (← links)
- Issues in machine-checking the decidability of implicational ticket entailment (Q1694477) (← links)
- A formally verified proof of the central limit theorem (Q1694568) (← links)
- Formally proving size optimality of sorting networks (Q1694569) (← links)
- On combining algebraic specifications with first-order logic via Athena (Q1697091) (← links)
- A semantic framework for proof evidence (Q1701039) (← links)
- Markov chains and Markov decision processes in Isabelle/HOL (Q1701041) (← links)
