The following pages link to Archive Formal Proofs (Q40327):
Displaying 50 items.
- Animating the Formalised Semantics of a Java-Like Language (Q3088008) (← links)
- Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism (Q3088012) (← links)
- Proof Pearl: The Marriage Theorem (Q3100219) (← links)
- Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm (Q3179390) (← links)
- Let’s Get Physical: Models and Methods for Real-World Security Protocols (Q3183515) (← links)
- Formalizing the Logic-Automaton Connection (Q3183526) (← links)
- A Certified Data Race Analysis for a Java-like Language (Q3183531) (← links)
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL (Q3183537) (← links)
- Unified Classical Logic Completeness (Q3192180) (← links)
- Interacting with Modal Logics in the Coq Proof Assistant (Q3194730) (← links)
- Formalization of Abstract State Transition Systems for SAT (Q3224685) (← links)
- A Mechanized Proof of Higman’s Lemma by Open Induction (Q3295156) (← links)
- Synthesis of distributed algorithms with parameterized threshold guards (Q3300835) (← links)
- Almost Event-Rate Independent Monitoring of Metric Temporal Logic (Q3303922) (← links)
- Para-Disagreement Logics and Their Implementation Through Embedding in Coq and SMT (Q3305339) (← links)
- Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments (Q3305694) (← links)
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics (Q3455772) (← links)
- Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors (Q3522072) (← links)
- Formal Proof: Reconciling Correctness and Understanding (Q3637280) (← links)
- The adequacy of Launchbury's natural semantics for lazy evaluation (Q4577822) (← links)
- Hoare Semigroups (Q4640310) (← links)
- Automated Verification of Parallel Nested DFS (Q5039512) (← links)
- Verified Certification of Reachability Checking for Timed Automata (Q5039522) (← links)
- Local Reasoning for Global Graph Properties (Q5041096) (← links)
- Proving the Safety of Highly-Available Distributed Objects (Q5041111) (← links)
- Quotients of Bounded Natural Functors (Q5048992) (← links)
- Deep Generation of Coq Lemma Names Using Elaborated Terms (Q5048996) (← links)
- Algebraically Closed Fields in Isabelle/HOL (Q5049003) (← links)
- Formalization of Forcing in Isabelle/ZF (Q5049004) (← links)
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL (Q5049005) (← links)
- Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation (Q5049007) (← links)
- Verified Approximation Algorithms (Q5049009) (← links)
- Efficient Verified Implementation of Introsort and Pdqsort (Q5049010) (← links)
- Verification of Closest Pair of Points Algorithms (Q5049012) (← links)
- Verifiable autonomy: From theory to applications (Q5054962) (← links)
- Bicategories in univalent foundations (Q5055496) (← links)
- Programming and Proving with Classical Types (Q5055999) (← links)
- Verified Root-Balanced Trees (Q5056001) (← links)
- Convolution and concurrency (Q5084483) (← links)
- Formalizing Ordinal Partition Relations Using Isabelle/HOL (Q5094473) (← links)
- Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL (Q5094474) (← links)
- Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras (Q5098718) (← links)
- A Hierarchy of Algebras for Boolean Subsets (Q5098719) (← links)
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL (Q5098720) (← links)
- (Q5111307) (← links)
- Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument (Q5126209) (← links)
- Programming and verifying a declarative first-order prover in Isabelle/HOL (Q5145439) (← links)
- An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata (Q5145684) (← links)
- Verified secure compilation for mixed-sensitivity concurrent programs (Q5152660) (← links)
- Automated Comparative Study of Some Generalized Rough Approximations (Q5164851) (← links)
