Pages that link to "Item:Q1600086"

The following pages link to Isabelle/HOL. A proof assistant for higher-order logic (Q1600086):

Displaying 50 items.

• The future of logic: foundation-independence (Q263104) (← links)
• Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (Q264193) (← links)
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
• The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
• Mechanizing complemented lattices within Mizar type system (Q286797) (← links)
• The higher-order prover \textsc{Leo}-II (Q287283) (← links)
• Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
• Eisbach: a proof method language for Isabelle (Q287365) (← links)
• Mechanizing a process algebra for network protocols (Q287372) (← links)
• A heuristic prover for real inequalities (Q287379) (← links)
• An algebraic approach to computations with progress (Q299188) (← links)
• Developments in concurrent Kleene algebra (Q299202) (← links)
• A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
• A two-valued logic for properties of strict functional programs allowing partial functions (Q352946) (← links)
• And so on \dots : reasoning with infinite diagrams (Q375286) (← links)
• A condensed semantics for qualitative spatial reasoning about oriented straight line segments (Q420800) (← links)
• \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps (Q429596) (← links)
• Invariant diagrams with data refinement (Q432148) (← links)
• ASP\(_{\text{fun}}\) : a typed functional active object calculus (Q433340) (← links)
• Combining decision procedures by (model-)equality propagation (Q436376) (← links)
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
• Conjecture synthesis for inductive theories (Q438543) (← links)
• Monotonicity inference for higher-order formulas (Q438558) (← links)
• Analytic tableaux for higher-order logic with choice (Q438561) (← links)
• Decreasing diagrams and relative termination (Q438562) (← links)
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
• Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (Q457250) (← links)
• Verification conditions for source-level imperative programs (Q465685) (← links)
• An inductive approach to strand spaces (Q470008) (← links)
• On theorem prover-based testing (Q470025) (← links)
• Recycling proof patterns in Coq: case studies (Q475385) (← links)
• Verification and code generation for invariant diagrams in Isabelle (Q478381) (← links)
• Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
• Reachability, confluence, and termination analysis with state-compatible automata (Q515687) (← links)
• Computer-assisted analysis of the Anderson-Hájek ontological controversy (Q523303) (← links)
• A framework for developing stand-alone certifiers (Q530847) (← links)
• Partial order semantics for use case and task models (Q539426) (← links)
• A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL (Q541222) (← links)
• Reachability analysis over term rewriting systems (Q556686) (← links)
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL (Q606999) (← links)
• Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving (Q617922) (← links)
• Trace-based verification of imperative programs with I/O (Q617977) (← links)
• Tactics for hierarchical proof (Q626933) (← links)
• Certifying compilers using higher-order theorem provers as certificate checkers (Q633302) (← links)
• Representing model theory in a type-theoretical logical framework (Q654913) (← links)
• Combining and automating classical and non-classical logics in classical higher-order logics (Q656826) (← links)
• Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points (Q670696) (← links)
• Amortized complexity verified (Q670702) (← links)
• Formal verification of an executable LTL model checker with partial order reduction (Q682350) (← links)
• Linear quantifier elimination (Q707743) (← links)