Pages that link to "Item:Q5327350"

The following pages link to Type Classes and Filters for Mathematical Analysis in Isabelle/HOL (Q5327350):

Displaying 35 items.

• Summable family in a commutative group (Q271890) (← links)
• Formal analysis of optical systems (Q475384) (← links)
• Groups -- additive notation. (Q491777) (← links)
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL (Q832721) (← links)
• Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation (Q1663216) (← links)
• A verified ODE solver and the Lorenz attractor (Q1663218) (← links)
• A formal proof in Coq of Lasalle's invariance principle (Q1687728) (← links)
• Bellerophon: tactical theorem proving for hybrid systems (Q1687737) (← links)
• A formally verified proof of the central limit theorem (Q1694568) (← links)
• Markov chains and Markov decision processes in Isabelle/HOL (Q1701041) (← links)
• The flow of ODEs: formalization of variational equation and Poincaré map (Q1722644) (← links)
• A consistent foundation for Isabelle/HOL (Q1739913) (← links)
• Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← links)
• Deductive stability proofs for ordinary differential equations (Q2233505) (← links)
• From LCF to Isabelle/HOL (Q2280211) (← links)
• Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL (Q2303242) (← links)
• An Isabelle/HOL formalisation of Green's theorem (Q2323451) (← links)
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109) (← links)
• An Isabelle/HOL Formalisation of Green’s Theorem (Q2829238) (← links)
• The Flow of ODEs (Q2829258) (← links)
• A Consistent Foundation for Isabelle/HOL (Q2945636) (← links)
• Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
• Mining the Archive of Formal Proofs (Q3453102) (← links)
• Formalization and Execution of Linear Algebra: From Theorems to Algorithms (Q3453644) (← links)
• Validating Mathematical Structures (Q5048998) (← links)
• Verification of Closest Pair of Points Algorithms (Q5049012) (← links)
• Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types (Q5094472) (← links)
• Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL (Q5094474) (← links)
• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL (Q5098720) (← links)
• (Q5195290) (← links)
• A certificate-based approach to formally verified approximations (Q5875414) (← links)
• Nine Chapters of Analytic Number Theory in Isabelle/HOL. (Q5875424) (← links)
• Mathematics and the formal turn (Q6130523) (← links)
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving (Q6639734) (← links)
• IsaVODEs: Interactive verification of cyber-physical systems at scale (Q6653093) (← links)