Archive Formal Proofs - MaRDI portal

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)

A Discrete Geometric Model of Concurrent Program Execution
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
Title not available (Why is that?)
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
Formal Proof: Reconciling Correctness and Understanding
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
Bicategories in univalent foundations
Formalization of the Poincaré disc model of hyperbolic geometry
Verified Approximation Algorithms
A comprehensive framework for saturation theorem proving
Deep Generation of Coq Lemma Names Using Elaborated Terms
\(\mathrm{HO}\pi\) in Coq
Formalising \(\varSigma\)-protocols and commitment schemes using crypthol
The Expressive Power of Monotonic Parallel Composition
CryptHOL: game-based proofs in higher-order logic
QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
Almost Event-Rate Independent Monitoring of Metric Temporal Logic
Soundness and completeness proofs by coinductive methods
A verified ODE solver and the Lorenz attractor
A verified SAT solver framework with learn, forget, restart, and incrementality
Mechanising a type-safe model of multithreaded Java with a verified compiler
The role of the Mizar mathematical library for interactive proof development in Mizar
Coupled similarity: the first 32 years
Formalizing complex plane geometry
Verified analysis of random binary tree structures
Equational Reasoning with Applicative Functors
On induction principles for partial orders
Simulink Timed Models for Program Verification
Verification of Closest Pair of Points Algorithms
A formally verified, optimized monitor for metric first-order dynamic logic
Interaction with formal mathematical documents in Isabelle/PIDE
Voting theory in the Lean theorem prover
Formalizing Ordinal Partition Relations Using Isabelle/HOL
Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13--17, 2015, Proceedings
Title not available (Why is that?)
A Hierarchy of Algebras for Boolean Subsets
Group of homography in real projective plane
Programming and verifying a declarative first-order prover in Isabelle/HOL
Verified iptables firewall analysis and verification
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
From LTL to deterministic automata. A safraless compositional approach
Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
Second-order properties of undirected graphs
Markov chains and Markov decision processes in Isabelle/HOL
The matrix reproved (verification pearl)
Unified Classical Logic Completeness
Formalization of Abstract State Transition Systems for SAT
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
A FORMAL PROOF OF THE KEPLER CONJECTURE
Automated verification of reactive and concurrent programs by calculation
Comprehending Isabelle/HOL’s Consistency
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
Formalizing the Edmonds-Karp Algorithm
Mechanical Verification of a Constructive Proof for FLP
POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
Animating the Formalised Semantics of a Java-Like Language
Proof Pearl: The Marriage Theorem
The flow of ODEs: formalization of variational equation and Poincaré map
Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
Friends with Benefits
Title not available (Why is that?)
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
Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
Mechanizing a process algebra for network protocols
Semi-intelligible Isar proofs from machine-generated proofs
A framework for the verification of certifying computations
Shared-Memory Multiprocessing for Interactive Theorem Proving
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
The adequacy of Launchbury's natural semantics for lazy evaluation
Verifying minimum spanning tree algorithms with Stone relation algebras
Building program construction and verification tools from algebraic principles
Formalization and implementation of modern SAT solvers
Automatic Functional Correctness Proofs for Functional Search Trees

This page was built for software: Archive Formal Proofs