Archive Formal Proofs
From MaRDI portal
Software:40327
No author found.
Related Items (only showing first 100 items - show all)
A complete semantics of \(\mathbb{K}\) and its translation to Isabelle ⋮ Strong eventual consistency of the collaborative editing framework WOOT ⋮ Formalizing geometric algebra in Lean ⋮ A modular first formalisation of combinatorial design theory ⋮ Beautiful formalizations in Isabelle/Naproche ⋮ Formalizing axiomatic systems for propositional logic in Isabelle/HOL ⋮ CICM'21 systems entries ⋮ A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Mechanizing a process algebra for network protocols ⋮ Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Lyndon words formalized in Isabelle/HOL ⋮ Proof pearl: Mechanizing the textbook proof of Huffman's algorithm ⋮ Formalization and implementation of modern SAT solvers ⋮ Automated verification of the parallel Bellman-Ford algorithm ⋮ A verified decision procedure for orders in Isabelle/HOL ⋮ Formalized soundness and completeness of epistemic logic ⋮ Verifying the conversion into CNF in dafny ⋮ Voting theory in the Lean theorem prover ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ Program logic for higher-order probabilistic programs in Isabelle/HOL ⋮ A two-valued logic for properties of strict functional programs allowing partial functions ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ A verified ODE solver and the Lorenz attractor ⋮ Verified iptables firewall analysis and verification ⋮ Mechanising a type-safe model of multithreaded Java with a verified compiler ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formalization of the resolution calculus for first-order logic ⋮ On induction principles for partial orders ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL ⋮ Subadditive and multiplicative ergodic theorems ⋮ Coupled similarity: the first 32 years ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ Invariant diagrams with data refinement ⋮ The matrix reproved (verification pearl) ⋮ Programmable hash functions and their applications ⋮ Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ Exploring the structure of an algebra text with locales ⋮ Maintaining a library of formal mathematics ⋮ The flow of ODEs: formalization of variational equation and Poincaré map ⋮ Formalizing network flow algorithms: a refinement approach in Isabelle/HOL ⋮ Growth of normalizing sequences in limit theorems for conservative maps ⋮ Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Safety of a smart classes-used regression test selection algorithm ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ Amortized complexity verified ⋮ Refinement to imperative HOL ⋮ Tarski geometry axioms. II ⋮ Cauchy mean theorem ⋮ A Perron-Frobenius theorem for deciding matrix growth ⋮ A verified implementation of the Berlekamp-Zassenhaus factorization algorithm ⋮ Formal verification of an executable LTL model checker with partial order reduction ⋮ Reachability, confluence, and termination analysis with state-compatible automata ⋮ Verifying minimum spanning tree algorithms with Stone relation algebras ⋮ (Co)inductive proof systems for compositional proofs in reachability logic ⋮ A framework for developing stand-alone certifiers ⋮ Unifying theories of reactive design contracts ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ A revision of the proof of the Kepler conjecture ⋮ An algebraic framework for minimum spanning tree problems ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ CoCon: a conference management system with formally verified document confidentiality ⋮ Formalising \(\varSigma\)-protocols and commitment schemes using crypthol ⋮ Interaction with formal mathematical documents in Isabelle/PIDE ⋮ Beginners' quest to formalize mathematics: a feasibility study in Isabelle ⋮ Tarski geometry axioms. III ⋮ Building program construction and verification tools from algebraic principles ⋮ Automated verification of reactive and concurrent programs by calculation ⋮ Distilling the requirements of Gödel's incompleteness theorems with a proof assistant ⋮ Automating free logic in HOL, with an experimental application in category theory ⋮ Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL ⋮ A verified implementation of algebraic numbers in Isabelle/HOL ⋮ Integration of formal proof into unified assurance cases with Isabelle/SACM ⋮ Adapting functional programs to higher order logic ⋮ A verified compiler from Isabelle/HOL to CakeML ⋮ Operating system verification---an overview ⋮ Interactive verification of architectural design patterns in FACTum ⋮ A formally verified, optimized monitor for metric first-order dynamic logic ⋮ Formalizing a Seligman-style tableau system for hybrid logic (short paper) ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory ⋮ A formalization of Dedekind domains and class groups of global fields ⋮ Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL ⋮ A formalization of the Smith normal form in higher-order logic ⋮ Binary codes that do not preserve primitivity ⋮ Synchronization modulo \(P\) in dynamic networks ⋮ A framework for the verification of certifying computations ⋮ A formalisation of the Myhill-Nerode theorem based on regular expressions ⋮ Extending Sledgehammer with SMT solvers ⋮ Proof pearl: A mechanized proof of GHC's mergesort ⋮ Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13--17, 2015, Proceedings ⋮ Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets ⋮ Labelings for decreasing diagrams ⋮ On the fine-structure of regular algebra ⋮ Formalizing complex plane geometry ⋮ Introduction to Liouville numbers
This page was built for software: Archive Formal Proofs
