The following pages link to Archive Formal Proofs (Q40327):
Displaying 50 items.
- All Liouville numbers are transcendental (Q2356937) (← links)
- Group of homography in real projective plane (Q2356938) (← 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)
- 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)
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema (Q2364696) (← links)
- Proof Pearl: regular expression equivalence and relation algebra (Q2392416) (← links)
- Automatic refinement to efficient data structures: a comparison of two approaches (Q2417948) (← links)
- Geographic wayfinders and space-time algebra (Q2423755) (← links)
- Derivatives and partial derivatives for regular shuffle expressions (Q2424692) (← links)
- How (not) to design strong-RSA signatures (Q2430687) (← links)
- Tight security for signature schemes without random oracles (Q2516531) (← links)
- A parameterized floating-point formalizaton in HOL Light (Q2520685) (← links)
- Some characterizations of the first-order functional calculus (Q2626397) (← links)
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools (Q2642981) (← links)
- Social choice theory in HOL. Arrow and Gibbard-Satterthwaite (Q2655324) (← links)
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started (Q2657827) (← links)
- Certified quantum computation in Isabelle/HOL (Q2666954) (← links)
- Certification of an exact worst-case self-stabilization time (Q2680867) (← links)
- Catoids and modal convolution algebras (Q2686581) (← links)
- Second-order properties of undirected graphs (Q2695354) (← links)
- Relation-algebraic verification of Borůvka's minimum spanning tree algorithm (Q2695356) (← links)
- A henkin-style completeness proof for the modal logic S5 (Q2695534) (← links)
- The Expressive Power of Monotonic Parallel Composition (Q2802500) (← links)
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
- POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl) (Q2829247) (← links)
- Mechanical Verification of a Constructive Proof for FLP (Q2829253) (← links)
- Formalizing the Edmonds-Karp Algorithm (Q2829260) (← links)
- Equational Reasoning with Applicative Functors (Q2829262) (← links)
- Automatic Functional Correctness Proofs for Functional Search Trees (Q2829265) (← links)
- Formalization of the Resolution Calculus for First-Order Logic (Q2829269) (← links)
- Formalized Timed Automata (Q2829277) (← links)
- Incompleteness, Undecidability and Automated Proofs (Q2829997) (← links)
- Simulink Timed Models for Program Verification (Q2842628) (← links)
- Truly Modular (Co)datatypes for Isabelle/HOL (Q2879246) (← links)
- Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm (Q2879261) (← links)
- Challenges and Experiences in Managing Large-Scale Proofs (Q2907311) (← links)
- Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm (Q2914741) (← links)
- Automated Reasoning in Higher-Order Regular Algebra (Q2915136) (← links)
- Layer Systems for Proving Confluence (Q2946770) (← links)
- Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion (Q2958390) (← links)
- A Discrete Geometric Model of Concurrent Program Execution (Q2971172) (← links)
- (Q2985126) (← links)
- A Lambda-Free Higher-Order Recursive Path Order (Q2988386) (← links)
- Friends with Benefits (Q2988636) (← links)
- Comprehending Isabelle/HOL’s Consistency (Q2988665) (← links)
- Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments (Q3087999) (← links)
