The following pages link to Archive Formal Proofs (Q40327):
Displayed 50 items.
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
- Integration of formal proof into unified assurance cases with Isabelle/SACM (Q2065527) (← links)
- A formally verified, optimized monitor for metric first-order dynamic logic (Q2096466) (← links)
- Formalizing a Seligman-style tableau system for hybrid logic (short paper) (Q2096470) (← links)
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory (Q2102926) (← links)
- A formalization of Dedekind domains and class groups of global fields (Q2102929) (← links)
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (Q2102946) (← links)
- A formalization of the Smith normal form in higher-order logic (Q2102950) (← links)
- Binary codes that do not preserve primitivity (Q2104527) (← links)
- Synchronization modulo \(P\) in dynamic networks (Q2110375) (← links)
- A complete semantics of \(\mathbb{K}\) and its translation to Isabelle (Q2119971) (← links)
- Strong eventual consistency of the collaborative editing framework WOOT (Q2121065) (← links)
- Formalizing geometric algebra in Lean (Q2128117) (← links)
- A modular first formalisation of combinatorial design theory (Q2128787) (← links)
- Beautiful formalizations in Isabelle/Naproche (Q2128789) (← links)
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL (Q2128791) (← links)
- CICM'21 systems entries (Q2128833) (← links)
- Automated verification of the parallel Bellman-Ford algorithm (Q2145339) (← links)
- A verified decision procedure for orders in Isabelle/HOL (Q2147186) (← links)
- Formalized soundness and completeness of epistemic logic (Q2148773) (← links)
- Verifying the conversion into CNF in dafny (Q2148786) (← links)
- Voting theory in the Lean theorem prover (Q2148823) (← links)
- Program logic for higher-order probabilistic programs in Isabelle/HOL (Q2163157) (← links)
- On induction principles for partial orders (Q2169127) (← links)
- CryptHOL: game-based proofs in higher-order logic (Q2175214) (← links)
- Subadditive and multiplicative ergodic theorems (Q2178267) (← links)
- Coupled similarity: the first 32 years (Q2182667) (← links)
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (Q2198135) (← links)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (Q2209537) (← links)
- Exploring the structure of an algebra text with locales (Q2209550) (← links)
- Maintaining a library of formal mathematics (Q2219408) (← links)
- Safety of a smart classes-used regression test selection algorithm (Q2229147) (← links)
- A Perron-Frobenius theorem for deciding matrix growth (Q2239274) (← links)
- Interaction with formal mathematical documents in Isabelle/PIDE (Q2287890) (← links)
- Beginners' quest to formalize mathematics: a feasibility study in Isabelle (Q2287895) (← links)
- Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← links)
- Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL (Q2303242) (← links)
- A verified implementation of algebraic numbers in Isabelle/HOL (Q2303244) (← links)
- A verified compiler from Isabelle/HOL to CakeML (Q2324018) (← links)
- Interactive verification of architectural design patterns in FACTum (Q2335950) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- A formalisation of the Myhill-Nerode theorem based on regular expressions (Q2351151) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- Proof pearl: A mechanized proof of GHC's mergesort (Q2351394) (← links)
- Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13--17, 2015, Proceedings (Q2351555) (← links)
- Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets (Q2352482) (← links)
- Labelings for decreasing diagrams (Q2352504) (← links)
- On the fine-structure of regular algebra (Q2352506) (← links)
- Formalizing complex plane geometry (Q2354913) (← links)
- Introduction to Liouville numbers (Q2356936) (← links)