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-1 functions, equipped with its C-1 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 Cinfinity functions. As an immediate application, we present a domain-theoretic generalization of Picard's theorem, which provides a data type for solving differential equations.