The following pages link to Interactive Theorem Proving (Q2829237):
Displayed 50 items.
- An Isabelle/HOL Formalisation of Green’s Theorem (Q2829238) (← links)
- HOL Zero’s Solutions for Pollack-Inconsistency (Q2829240) (← links)
- Infeasible Paths Elimination by Symbolic Execution Techniques (Q2829242) (← links)
- Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency (Q2829245) (← links)
- POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl) (Q2829247) (← links)
- CoSMed: A Confidentiality-Verified Social Media Platform (Q2829248) (← links)
- Mechanical Verification of a Constructive Proof for FLP (Q2829253) (← links)
- Visual Theorem Proving with the Incredible Proof Machine (Q2829254) (← links)
- Proof Pearl: Bounding Least Common Multiples with Triangles (Q2829255) (← links)
- Two-Way Automata in Coq (Q2829256) (← links)
- Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms (Q2829257) (← links)
- The Flow of ODEs (Q2829258) (← links)
- From Types to Sets by Local Type Definitions in Higher-Order Logic (Q2829259) (← links)
- Formalizing the Edmonds-Karp Algorithm (Q2829260) (← links)
- A Formal Proof of Cauchy’s Residue Theorem (Q2829261) (← links)
- Equational Reasoning with Applicative Functors (Q2829262) (← links)
- Formally Verified Approximations of Definite Integrals (Q2829263) (← links)
- Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems (Q2829264) (← links)
- Automatic Functional Correctness Proofs for Functional Search Trees (Q2829265) (← links)
- A Framework for the Automatic Formal Verification of Refinement from Cogent to C (Q2829268) (← links)
- Formalization of the Resolution Calculus for First-Order Logic (Q2829269) (← links)
- Verified Operational Transformation for Trees (Q2829271) (← links)
- Hereditarily Finite Sets in Constructive Type Theory (Q2829273) (← links)
- Algebraic Numbers in Isabelle/HOL (Q2829274) (← links)
- Modular Dependent Induction in Coq, Mendler-Style (Q2829276) (← links)
- Formalized Timed Automata (Q2829277) (← links)
- AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic (Q2829278) (← links)
- What’s in a Theorem Name? (Q2829279) (← links)
- Cardinalities of Finite Relations in Coq (Q2829280) (← links)
- Formalising Semantics for Expected Running Time of Probabilistic Programs (Q2829281) (← links)
- On the Formalization of Fourier Transform in Higher-order Logic (Q2829282) (← links)
- CoqPIE: An IDE Aimed at Improving Proof Development Productivity (Q2829283) (← links)
- Towards a Formally Verified Proof Assistant (Q2879241) (← links)
- Implicational Rewriting Tactics in HOL (Q2879242) (← links)
- A Heuristic Prover for Real Inequalities (Q2879243) (← links)
- A Formal Library for Elliptic Curves in the Coq Proof Assistant (Q2879245) (← links)
- Truly Modular (Co)datatypes for Isabelle/HOL (Q2879246) (← links)
- Cardinals in Isabelle/HOL (Q2879247) (← links)
- Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code (Q2879248) (← links)
- Showing Invariance Compositionally for a Process Algebra for Network Protocols (Q2879249) (← links)
- A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) (Q2879250) (← links)
- From Operational Models to Information Theory; Side Channels in pGCL with Isabelle (Q2879251) (← links)
- A Coq Formalization of Finitely Presented Modules (Q2879252) (← links)
- Formalized, Effective Domain Theory in Coq (Q2879253) (← links)
- Completeness and Decidability Results for CTL in Coq (Q2879254) (← links)
- Hypermap Specification and Certified Linked Implementation Using Orbits (Q2879255) (← links)
- A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction (Q2879257) (← links)
- Experience Implementing a Performant Category-Theory Library in Coq (Q2879258) (← links)
- A New and Formalized Proof of Abstract Completion (Q2879259) (← links)
- HOL with Definitions: Semantics, Soundness, and a Verified Implementation (Q2879260) (← links)