Domain Theory and Differential Calculus (Functions of one variable)
We introduce a domain-theoretic framework for differential calculus, which aims to synthesize differentiable mathematics and computer science. We define the indefinite 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 continuously differentiable classical functions 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. As an immediate application, we present a domain-theoretic generalization of Picard's theorem, which provides a data type for solving differential equations.