The following pages link to Isabelle (Q13212):
Displaying 50 items.
- The future of logic: foundation-independence (Q263104) (← links)
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Interactive theorem proving. Preface of the special issue (Q287356) (← links)
- On definitions of constants and types in HOL (Q287358) (← links)
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (Q287361) (← links)
- Eisbach: a proof method language for Isabelle (Q287365) (← links)
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (Q333325) (← links)
- A scalable module system (Q391632) (← links)
- Programming and automating mathematics in the Tarski-Kleene hierarchy (Q406433) (← links)
- Fractional variational integrators for fractional variational problems (Q430324) (← links)
- Conjecture synthesis for inductive theories (Q438543) (← links)
- Monotonicity inference for higher-order formulas (Q438558) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Certifying algorithms (Q465678) (← links)
- An inductive approach to strand spaces (Q470008) (← links)
- Verification and code generation for invariant diagrams in Isabelle (Q478381) (← links)
- Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
- Automated type-based analysis of injective agreement in the presence of compromised principals (Q492914) (← links)
- An introduction to mechanized reasoning (Q504394) (← links)
- Reachability, confluence, and termination analysis with state-compatible automata (Q515687) (← links)
- Proving linearizability with temporal logic (Q539223) (← links)
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling (Q540694) (← links)
- Reasoning about conditional probabilities in a higher-order-logic theorem prover (Q545151) (← links)
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL (Q606999) (← links)
- Automated flaw detection in algebraic specifications (Q616853) (← links)
- Reasoning about memory layouts (Q633298) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- Automating Event-B invariant proofs by rippling and proof patching (Q667526) (← 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)
- A new approach to abstract syntax with variable binding (Q699761) (← links)
- The world's shortest correct exact real arithmetic program? (Q714620) (← links)
- Implementing type systems for the IDE with Xsemantics (Q739624) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- Implementing geometric algebra products with binary trees (Q742367) (← links)
- A shape graph logic and a shape system (Q744329) (← links)
- Experiments with proof plans for induction (Q809617) (← links)
- Towards a trustworthy semantics-based language framework via proof generation (Q832282) (← links)
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (Q832723) (← links)
- Lyndon words formalized in Isabelle/HOL (Q832940) (← links)
- Proving fairness and implementation correctness of a microkernel scheduler (Q835766) (← links)
- Balancing the load. Leveraging a semantics stack for systems verification (Q835780) (← links)
- Proof pearl: Mechanizing the textbook proof of Huffman's algorithm (Q839031) (← links)
- Simplifying proofs in Fitch-style natural deduction systems (Q851139) (← links)
- Ordinal arithmetic: Algorithms and mechanization (Q851144) (← links)
- TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
