Cited in
(36)- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- A formal proof of Cauchy's residue theorem
- A formalization of properties of continuous functions on closed intervals
- A Coq formalization of Lebesgue integration of nonnegative functions
- The flow of ODEs: formalization of variational equation and Poincaré map
- Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Simple type theory is not too simple: Grothendieck's schemes without dependent types
- Formally verified approximations of definite integrals
- C-CoRN
- Flocq
- dReach
- Bellerophon
- TiML
- Lp spaces
- QuickSort Cost
- Ordinary Differential Equations
- Mathematical Components
- Algebraic_VCs
- KAD
- Formally verified approximations of definite integrals
- mathlib
- Verified tail bounds for randomized programs
- CBench
- Quantales
- Transformer semantics
- Formalization techniques for asymptotic reasoning in classical analysis
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
- Validating Mathematical Structures
- Computational logic: its origins and applications
- finmap
- PCM library
- HolPy
- Free modal Riesz spaces are Archimedean: a syntactic proof
- A formal proof in Coq of Lasalle's invariance principle
- Bellerophon: tactical theorem proving for hybrid systems
This page was built for software: Coquelicot
