Domain theory and differential calculus (functions of one variable)

A data-type for differential calculus is introduced, which is based on domain theory. We define the integral and also the derivative of a Scott continuous function on the domain of intervals, and present a domain-theoretic generalization of the fundamental theorem of calculus. We then construct a domain for differentiable real valued functions of a real variable. The set of classical C¹ functions, equipped with its C¹ norm, is embedded into the set of maximal elements of this domain, which is a countably based bounded complete continuous domain. This gives a data type for differential calculus. The construction can be generalized to C^k and C^∞ functions. As an immediate application, we present a domain-theoretic generalization of Picard´s theorem, which provides a data type for solving differential equations.