Cited in
(only showing first 100 items - show all)- Comprehending Isabelle/HOL’s Consistency
- Subadditive and multiplicative ergodic theorems
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- Tight security for signature schemes without random oracles
- Para-disagreement logics and their implementation through embedding in Coq and SMT
- Mechanizing \textit{Principia logico-metaphysica} in functional type-theory
- scientific article; zbMATH DE number 7649976 (Why is no real title available?)
- Formal verification of an executable LTL model checker with partial order reduction
- Growth of normalizing sequences in limit theorems for conservative maps
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- CoCon: a conference management system with formally verified document confidentiality
- A framework for developing stand-alone certifiers
- Extending Sledgehammer with SMT solvers
- A formalization of Dedekind domains and class groups of global fields
- A formalization of the Smith normal form in higher-order logic
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Binary codes that do not preserve primitivity
- Programming and Proving with Classical Types
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- Lyndon words formalized in Isabelle/HOL
- Reasoning about cardinalities of relations with applications supported by proof assistants
- Tarski geometry axioms. III
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- On the fine-structure of regular algebra
- FindFacts
- SErAPIS
- Maintaining a library of formal mathematics
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
- A Mechanized Proof of Higman’s Lemma by Open Induction
- Synchronization modulo \(P\) in dynamic networks
- Formalizing ordinal partition relations using Isabelle/HOL
- A verified implementation of algebraic numbers in Isabelle/HOL
- Proof pearl: Mechanizing the textbook proof of Huffman's algorithm
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- Adapting functional programs to higher order logic
- (Co)inductive proof systems for compositional proofs in reachability logic
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras
- Refinement to imperative HOL
- Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
- A complete semantics of \(\mathbb{K}\) and its translation to Isabelle
- Safety of a smart classes-used regression test selection algorithm
- Automatic functional correctness proofs for functional search trees
- Combining source, content, presentation, narration, and relational representation
- The flow of ODEs: formalization of variational equation and Poincaré map
- The expressive power of monotonic parallel composition
- Mechanical Verification of a Constructive Proof for FLP
- POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
- scientific article; zbMATH DE number 7649964 (Why is no real title available?)
- scientific article; zbMATH DE number 7649970 (Why is no real title available?)
- Formal Proof: Reconciling Correctness and Understanding
- Proving the safety of highly-available distributed objects
- Variants of Gödel's ontological proof in a natural deduction calculus
- Almost event-rate independent monitoring of metric temporal logic
- Proof pearl: A mechanized proof of GHC's mergesort
- Convolution and concurrency
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL
- Unifying theories of reactive design contracts
- Interactive verification of architectural design patterns in FACTum
- Strong eventual consistency of the collaborative editing framework WOOT
- Taming multirelations
- Formalization of the resolution calculus for first-order logic
- Mechanizing a process algebra for network protocols
- Semi-intelligible Isar proofs from machine-generated proofs
- Formalizing the Logic-Automaton Connection
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- Formalization of the Poincaré disc model of hyperbolic geometry
- Bicategories in univalent foundations
- Formalizing geometric algebra in Lean
- A modular first formalisation of combinatorial design theory
- Beautiful formalizations in Isabelle/Naproche
- CICM'21 systems entries
- Invariant diagrams with data refinement
- Programmable hash functions and their applications
- A framework for the verification of certifying computations
- Applying data refinement for monadic programs to Hopcroft's algorithm
- Some characterizations of the first-order functional calculus
- Truly modular (co)datatypes for Isabelle/HOL
- Relation-algebraic verification of Prim's minimum spanning tree algorithm
- A verified compiler from Isabelle/HOL to CakeML
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- Hoare semigroups
- A formal proof of the Kepler conjecture
- A parameterized floating-point formalizaton in HOL Light
- Verified Approximation Algorithms
- Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors
- scientific article; zbMATH DE number 7649968 (Why is no real title available?)
- Verifying minimum spanning tree algorithms with Stone relation algebras
- Local reasoning for global graph properties
- The adequacy of Launchbury's natural semantics for lazy evaluation
- Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments
- scientific article; zbMATH DE number 7204430 (Why is no real title available?)
- Automated verification of parallel nested DFS
- Building program construction and verification tools from algebraic principles
- Simulink timed models for program verification
- A comprehensive framework for saturation theorem proving
- All Liouville numbers are transcendental
- Introduction to Liouville numbers
- Formalization and implementation of modern SAT solvers
- Deep Generation of Coq Lemma Names Using Elaborated Terms
This page was built for software: Archive Formal Proofs
