The theory of analysis in Isabelle/HOL derives from earlier formalizations that were limited to specific concrete types: ℝ, ℂ and ℝn. Isabelle's new analysis theory unifies and generalizes these earlier efforts. The improvements are centered on two primary contributions: a generic theory of limits based on filters, and a new hierarchy of type classes that includes various topological, metric, vector, and algebraic spaces. These let us apply many results in multivariate analysis to types which are not Euclidean spaces, such as the extended real numbers, bounded continuous functions, or finite maps. © 2013 Springer-Verlag.
CITATION STYLE
Hölzl, J., Immler, F., & Huffman, B. (2013). Type classes and filters for mathematical analysis in Isabelle/HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7998 LNCS, pp. 279–294). https://doi.org/10.1007/978-3-642-39634-2_21
Mendeley helps you to discover research relevant for your work.