The following pages link to Isabelle/HOL (Q14275):
Displaying 50 items.
- Formalizing provable anonymity in Isabelle/HOL (Q2355379) (← links)
- Theorem proving graph grammars with attributes and negative application conditions (Q2358623) (← links)
- Using relation-algebraic means and tool support for investigating and computing bipartitions (Q2360655) (← links)
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (Q2360872) (← links)
- A decision procedure for (co)datatypes in SMT solvers (Q2360873) (← links)
- Proving divide and conquer complexities in Isabelle/HOL (Q2362108) (← links)
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109) (← links)
- Analyzing program termination and complexity automatically with \textsf{AProVE} (Q2362493) (← links)
- Automatically proving termination and memory safety for programs with pointer arithmetic (Q2362494) (← links)
- Soundness and completeness proofs by coinductive methods (Q2362498) (← links)
- Variants of Gödel's ontological proof in a natural deduction calculus (Q2363503) (← links)
- From LTL to deterministic automata. A safraless compositional approach (Q2363815) (← links)
- A verified algorithm enumerating event structures (Q2364684) (← links)
- Classification of alignments between concepts of formal mathematical systems (Q2364703) (← links)
- Automating change of representation for proofs in discrete mathematics (extended version) (Q2364883) (← links)
- The gauge integral theory in HOL4 (Q2375421) (← links)
- A unified framework for DPLL(T) + certificates (Q2375732) (← links)
- Invariants for the FoCaL language (Q2379680) (← links)
- Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006. Proceedings (Q2382312) (← links)
- Semantics, calculi, and analysis for object-oriented specifications (Q2390933) (← links)
- Proof Pearl: regular expression equivalence and relation algebra (Q2392416) (← links)
- A canonical locally named representation of binding (Q2392482) (← links)
- Formalizing adequacy: a case study for higher-order abstract syntax (Q2392483) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- Predictive runtime enforcement (Q2402553) (← links)
- Efficient certified RAT verification (Q2405252) (← links)
- Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems (Q2405266) (← links)
- Certifying safety and termination proofs for integer transition systems (Q2405269) (← links)
- A proof strategy language and proof script generation for Isabelle/HOL (Q2405272) (← links)
- A formal, resource consumption-preserving translation of actors to Haskell (Q2409724) (← links)
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency (Q2414249) (← links)
- Automatic refinement to efficient data structures: a comparison of two approaches (Q2417948) (← links)
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example (Q2418046) (← links)
- A corrected quantitative version of the Morse lemma (Q2421532) (← links)
- Finite integer computations: An algebraic foundation for their correctness (Q2432238) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation (Q2437794) (← links)
- Why do the relativistic masses and momenta of faster-than-light particles decrease as their speeds increase? (Q2447862) (← links)
- Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates (Q2457362) (← links)
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book (Q2462639) (← links)
- A program logic for resources (Q2463560) (← links)
- Translating higher-order clauses to first-order clauses (Q2471742) (← links)
- Proving pointer programs in higher-order logic (Q2486585) (← links)
- Mathematical software -- ICMS 2016. 5th international conference, Berlin, Germany, July 11--14, 2016. Proceedings (Q2630690) (← links)
- From informal to formal proofs in Euclidean geometry (Q2631958) (← links)
- Portfolio theorem proving and prover runtime prediction for geometry (Q2631959) (← links)
- A decision procedure for linear ``big O'' equations (Q2642465) (← links)
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools (Q2642981) (← links)
- Code-carrying theories (Q2643124) (← links)
- Social choice theory in HOL. Arrow and Gibbard-Satterthwaite (Q2655324) (← links)
