Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
From MaRDI portal
Publication:5327350
DOI10.1007/978-3-642-39634-2_21zbMath1317.68213OpenAlexW2174838357MaRDI QIDQ5327350
Fabian Immler, Johannes Hölzl, Brian Huffman
Publication date: 7 August 2013
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-39634-2_21
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (35)
Summable family in a commutative group ⋮ A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Unnamed Item ⋮ Validating Mathematical Structures ⋮ Verification of Closest Pair of Points Algorithms ⋮ Mining the Archive of Formal Proofs ⋮ Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ A verified ODE solver and the Lorenz attractor ⋮ Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types ⋮ Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL ⋮ A Consistent Foundation for Isabelle/HOL ⋮ Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL ⋮ A formal proof in Coq of Lasalle's invariance principle ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ Formalising Mathematics in Simple Type Theory ⋮ Mathematics and the formal turn ⋮ A formally verified proof of the central limit theorem ⋮ A formalization of the change of variables formula for integrals in mathlib ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ The flow of ODEs: formalization of variational equation and Poincaré map ⋮ Formal analysis of optical systems ⋮ Nine Chapters of Analytic Number Theory in Isabelle/HOL. ⋮ A certificate-based approach to formally verified approximations ⋮ Groups -- additive notation. ⋮ Deductive stability proofs for ordinary differential equations ⋮ A consistent foundation for Isabelle/HOL ⋮ Coquelicot: a user-friendly library of real analysis for Coq ⋮ From LCF to Isabelle/HOL ⋮ Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL ⋮ An Isabelle/HOL Formalisation of Green’s Theorem ⋮ The Flow of ODEs ⋮ An Isabelle/HOL formalisation of Green's theorem
Uses Software
This page was built for publication: Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
