Isabelle/HOL

No author found.

Related Items (only showing first 100 items - show all)

Verifying hybrid systems with modal Kleene algebra ⋮ A set solver for finite set relation algebra ⋮ Layer systems for confluence -- formalized ⋮ How testing helps to diagnose proof failures ⋮ Tests and proofs for custom data generators ⋮ Formal analysis of the kinematic Jacobian in screw theory ⋮ Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques ⋮ Nominal unification with atom-variables ⋮ Aligning concepts across proof assistant libraries ⋮ Program extraction for mutable arrays ⋮ Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings ⋮ Introduction to ``Milestones in interactive theorem proving ⋮ Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ A verified ODE solver and the Lorenz attractor ⋮ CoSMed: a confidentiality-verified social media platform ⋮ Verified iptables firewall analysis and verification ⋮ Mechanising a type-safe model of multithreaded Java with a verified compiler ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formalization of the resolution calculus for first-order logic ⋮ A deontic logic reasoning infrastructure ⋮ Mechanized proofs of opacity: a comparison of two techniques ⋮ A formal proof generator from semi-formal proof documents ⋮ Foundational (co)datatypes and (co)recursion for higher-order logic ⋮ Automated theory exploration for interactive theorem proving: an introduction to the Hipster system ⋮ How to simulate it in Isabelle: towards formal proof for secure multi-party computation ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ Efficient, verified checking of propositional proofs ⋮ Proof tactics for assertions in separation logic ⋮ Gauge integral ⋮ Reasoning about algebraic data types with abstractions ⋮ A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. ⋮ Issues in machine-checking the decidability of implicational ticket entailment ⋮ A formally verified proof of the central limit theorem ⋮ Formally proving size optimality of sorting networks ⋮ On combining algebraic specifications with first-order logic via Athena ⋮ Verified bytecode subroutines ⋮ Bytecode verification by model checking ⋮ A semantic framework for proof evidence ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ Unifying theories of time with generalised reactive processes ⋮ Towards verification of cyber-physical systems with UTP and Isabelle/HOL ⋮ Formal proof of a machine closed theorem in Coq ⋮ The flow of ODEs: formalization of variational equation and Poincaré map ⋮ From types to sets by local type definition in higher-order logic ⋮ Formalizing network flow algorithms: a refinement approach in Isabelle/HOL ⋮ Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL ⋮ Refinement to imperative HOL ⋮ A consistent foundation for Isabelle/HOL ⋮ Completeness in PVS of a nominal unification algorithm ⋮ A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols ⋮ External and internal syntax of the \(\lambda \)-calculus ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ The axiomatization of override and update ⋮ A revision of the proof of the Kepler conjecture ⋮ Organizing numerical theories using axiomatic type classes ⋮ Relation algebra as programming language using the Ampersand compiler ⋮ An algebraic framework for minimum spanning tree problems ⋮ An abstract model for proving safety of autonomous urban traffic ⋮ Physical addressing on real hardware in Isabelle/HOL ⋮ Formalizing ring theory in PVS ⋮ Software tool support for modular reasoning in modal logics of actions ⋮ Backwards and forwards with separation logic ⋮ Tactics and certificates in Meta Dedukti ⋮ A formalization of the LLL basis reduction algorithm ⋮ A formal proof of the minor-exclusion property for treewidth-two graphs ⋮ ProofWatch: watchlist guidance for large theories in E ⋮ Verifying the LTL to Büchi automata translation via very weak alternating automata ⋮ Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) ⋮ Fast machine words in Isabelle/HOL ⋮ Relational parametricity and quotient preservation for modular (co)datatypes ⋮ Towards verified handwritten calculational proofs (short paper) ⋮ A formally verified solver for homogeneous linear Diophantine equations ⋮ Boosting the reuse of formal specifications ⋮ Towards formal foundations for game theory ⋮ Program verification in the presence of cached address translation ⋮ Verified tail bounds for randomized programs ⋮ Verified memoization and dynamic programming ⋮ \(\mathrm{MDP + TA = PTA}\): probabilistic timed automata, formalized (short paper) ⋮ Formalization of a polymorphic subtyping algorithm ⋮ Tarski geometry axioms. III ⋮ Klein-Beltrami model. I ⋮ Klein-Beltrami model. II ⋮ Fubini's theorem for non-negative or non-positive functions ⋮ Using the Isabelle ontology framework -- linking the formal with the informal ⋮ Concrete semantics with Coq and CoqHammer ⋮ Isabelle import infrastructure for the Mizar Mathematical Library ⋮ Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL ⋮ Goal-oriented conjecturing for Isabelle/HOL ⋮ Superposition for \(\lambda\)-free higher-order logic ⋮ The higher-order prover Leo-III ⋮ Superposition with datatypes and codatatypes ⋮ Verifying asymptotic time complexity of imperative programs in Isabelle ⋮ ATPboost: learning premise selection in binary setting with ATP feedback ⋮ Efficiently checking propositional refutations in HOL theorem provers ⋮ On the correctness of upper layers of automotive systems ⋮ Winskel is (almost) right: Towards a mechanized semantics textbook ⋮ Operating system verification---an overview ⋮ Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings ⋮ More Church-Rosser proofs (in Isabelle/HOL) ⋮ Isabelle/HOL. A proof assistant for higher-order logic

This page was built for software: Isabelle/HOL