  We present a simple functional programming language, called Dual PCF, that
implements forward mode automatic differentiation using dual numbers in the
framework of exact real number computation. The main new feature of this
language is the ability to evaluate correctly up to the precision specified by
the user -- in a simple and direct way -- the directional derivative of
functionals as well as first order functions. In contrast to other comparable
languages, Dual PCF also includes the recursive operator for defining functions
and functionals. We provide a wide range of examples of Lipschitz functions and
functionals that can be defined in Dual PCF. We use domain theory both to give
a denotational semantics to the language and to prove the correctness of the
new derivative operator using logical relations. To be able to differentiate
functionals -- including on function spaces equipped with their compact-open
topology that do not admit a norm -- we develop a domain-theoretic directional
derivative that is Scott continuous and extends Clarke's subgradient of
real-valued locally Lipschitz maps on Banach spaces to real-valued continuous
maps on Hausdorff topological vector spaces. Finally, we show that we can
express arbitrary computable linear functionals in Dual PCF.
