analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
Exact real computer arithmetic refers to treatment of real number arithmetic on computers to finite (necessarily) but arbitrary precision. This is in contrast with what is called floating-point arithmetic? which uses just one fixed finite approximation of the real numbers by natural numbers.
Exact real computer arithmetic essentially implements what in mathematical computability theory is known as the type-II theory (in contrast to the “type-I” theory of partial recursive functions acting just on natural numbers). The formal mathematical definition of computable function (analysis) is the core topic of constructive analysis/exact analysis.
Discussion of implementation of exact real computer arithmetic includes
Discussion relating to computability theory, Type Two Theory of Effectivity and constructive analysis/computable analysis includes
Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk, Constructive analysis, types and exact real numbers, 2006 (pdf)
The Haskell Wiki, Exact real arithmetic
A collection of further references is listed at