Archive Formal Proofs

swMATH28613MaRDI QIDQ40327FDOQ40327

Author name not available (Why is that?)

Described by source

• Mining the Archive of Formal Proofs

Cited In (only showing first 100 items - show all)

• Mechanizing \textit{Principia logico-metaphysica} in functional type-theory
• Extending Sledgehammer with SMT solvers
• CoCon: a conference management system with formally verified document confidentiality
• Formal verification of an executable LTL model checker with partial order reduction
• A framework for developing stand-alone certifiers
• Tarski geometry axioms. III
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• On the fine-structure of regular algebra
• Maintaining a library of formal mathematics
• Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
• Automatic functional correctness proofs for functional search trees
• Mechanical Verification of a Constructive Proof for FLP
• POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
• The flow of ODEs: formalization of variational equation and Poincaré map
• Taming multirelations
• Formalization of the resolution calculus for first-order logic
• Formalizing the Logic-Automaton Connection
• Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
• Mechanizing a process algebra for network protocols
• Semi-intelligible Isar proofs from machine-generated proofs
• Applying data refinement for monadic programs to Hopcroft's algorithm
• A framework for the verification of certifying computations
• Relation-algebraic verification of Prim's minimum spanning tree algorithm
• Truly modular (co)datatypes for Isabelle/HOL
• Hoare semigroups
• A verified compiler from Isabelle/HOL to CakeML
• Invariant diagrams with data refinement
• Programmable hash functions and their applications
• Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors
• Local reasoning for global graph properties
• The adequacy of Launchbury's natural semantics for lazy evaluation
• Verifying minimum spanning tree algorithms with Stone relation algebras
• Automated verification of parallel nested DFS
• Building program construction and verification tools from algebraic principles
• Formalization and implementation of modern SAT solvers
• Proving divide and conquer complexities in Isabelle/HOL
• Cardinality of relations and relational approximation algorithms
• Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Formalization of the Resolution Calculus for First-Order Logic
• Formalized soundness and completeness of epistemic logic
• Proof Pearl: regular expression equivalence and relation algebra
• A learning-based fact selector for Isabelle/HOL
• A Perron-Frobenius theorem for deciding matrix growth
• Challenges and experiences in managing large-scale proofs
• A Certified Data Race Analysis for a Java-like Language
• Shared-memory multiprocessing for interactive theorem proving
• Verified decision procedures for MSO on words based on derivatives of regular expressions
• Interactive theorem proving from the perspective of Isabelle/Isar
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• An algebraic framework for minimum spanning tree problems
• A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
• Operating system verification---an overview
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• A two-valued logic for properties of strict functional programs allowing partial functions
• Psi-calculi in Isabelle
• Extending Sledgehammer with SMT solvers
• A decision procedure for (co)datatypes in SMT solvers
• How (not) to design strong-RSA signatures
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Verified Root-Balanced Trees
• Verification of clock synchronization algorithms: experiments on a combination of deductive tools
• Cauchy mean theorem
• Tarski geometry axioms. II
• Partial and nested recursive function definitions in higher-order logic
• Verified certification of reachability checking for timed automata
• A revision of the proof of the Kepler conjecture
• Animating the formalised semantics of a Java-like language
• Proof pearl: the marriage theorem
• Efficient Verified Implementation of Introsort and Pdqsort
• Automated Reasoning in Higher-Order Regular Algebra
• Amortized complexity verified
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Reachability, confluence, and termination analysis with state-compatible automata
• Verified efficient implementation of Gabow's strongly connected component algorithm
• Formalizing the Edmonds-Karp algorithm
• Friends with benefits. Implementing corecursion in foundational proof assistants
• Stone relation algebras
• Verified efficient enumeration of plane graphs modulo isomorphism
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Interacting with Modal Logics in the Coq Proof Assistant
• Subadditive and multiplicative ergodic theorems
• Growth of normalizing sequences in limit theorems for conservative maps
• Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
• Lyndon words formalized in Isabelle/HOL
• Formalizing ordinal partition relations using Isabelle/HOL
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• (Co)inductive proof systems for compositional proofs in reachability logic
• Proof pearl: Mechanizing the textbook proof of Huffman's algorithm
• Adapting functional programs to higher order logic
• Refinement to imperative HOL
• The expressive power of monotonic parallel composition
• Formal Proof: Reconciling Correctness and Understanding
• Almost event-rate independent monitoring of metric temporal logic
• Proof pearl: A mechanized proof of GHC's mergesort
• Formalizing axiomatic systems for propositional logic in Isabelle/HOL
• Unifying theories of reactive design contracts
• Interactive verification of architectural design patterns in FACTum

This page was built for software: Archive Formal Proofs