Type classes and filters for mathematical analysis in Isabelle/HOL

ITP, pp. 279-294, 2013.

Cited by: 16|Bibtex|Views0|
EI
Other Links: dl.acm.org|dblp.uni-trier.de|academic.microsoft.com
Keywords:
extended real numberalgebraic spacegeneric theorybounded continuous functiontype classMore(7+)

Abstract:

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 ...More

Code:

Data:

Your rating :
0

 

Tags
Comments