The following pages link to Archive Formal Proofs (Q40327):
Displaying 50 items.
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Mechanizing a process algebra for network protocols (Q287372) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (Q333325) (← links)
- A two-valued logic for properties of strict functional programs allowing partial functions (Q352946) (← links)
- Invariant diagrams with data refinement (Q432148) (← links)
- Programmable hash functions and their applications (Q434345) (← links)
- Tarski geometry axioms. II (Q502683) (← links)
- Cauchy mean theorem (Q502698) (← links)
- Reachability, confluence, and termination analysis with state-compatible automata (Q515687) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL (Q606999) (← links)
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (Q670699) (← links)
- Amortized complexity verified (Q670702) (← links)
- Formal verification of an executable LTL model checker with partial order reduction (Q682350) (← links)
- Building program construction and verification tools from algebraic principles (Q736461) (← links)
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL (Q832721) (← links)
- Lyndon words formalized in Isabelle/HOL (Q832940) (← links)
- Proof pearl: Mechanizing the textbook proof of Huffman's algorithm (Q839031) (← links)
- Formalization and implementation of modern SAT solvers (Q839035) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- A revision of the proof of the Kepler conjecture (Q977177) (← links)
- Adapting functional programs to higher order logic (Q1029815) (← links)
- Operating system verification---an overview (Q1040002) (← links)
- The role of the Mizar mathematical library for interactive proof development in Mizar (Q1663215) (← links)
- A verified ODE solver and the Lorenz attractor (Q1663218) (← links)
- Verified iptables firewall analysis and verification (Q1663231) (← links)
- Mechanising a type-safe model of multithreaded Java with a verified compiler (Q1663233) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- Markov chains and Markov decision processes in Isabelle/HOL (Q1701041) (← links)
- The matrix reproved (verification pearl) (Q1703015) (← links)
- The flow of ODEs: formalization of variational equation and Poincaré map (Q1722644) (← links)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (Q1722647) (← links)
- Growth of normalizing sequences in limit theorems for conservative maps (Q1725491) (← links)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844) (← links)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 (Q1731963) (← links)
- Refinement to imperative HOL (Q1739909) (← links)
- An algebraic framework for minimum spanning tree problems (Q1786562) (← links)
- Tarski geometry axioms. III (Q1795563) (← links)
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (Q1984794) (← links)
- Verifying minimum spanning tree algorithms with Stone relation algebras (Q1994364) (← links)
- (Co)inductive proof systems for compositional proofs in reachability logic (Q1996855) (← links)
- Unifying theories of reactive design contracts (Q2007732) (← links)
- Formalization of the Poincaré disc model of hyperbolic geometry (Q2031408) (← links)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
- CoCon: a conference management system with formally verified document confidentiality (Q2031419) (← links)
- Formalising \(\varSigma\)-protocols and commitment schemes using crypthol (Q2031427) (← links)
- Automated verification of reactive and concurrent programs by calculation (Q2043817) (← links)
