A coherent differential PCF

The categorical models of the differential lambda-calculus are additivecategories because of the Leibniz rule which requires the summation of twoexpressions. This means that, as far as the differential lambda-calculus anddifferential linear logic are concerned, these models feature finitenon-determinism and indeed these languages are essentially non-deterministic.In a previous paper we introduced a categorical framework for differentiationwhich does not require additivity and is compatible with deterministic modelssuch as coherence spaces and probabilistic models such as probabilisticcoherence spaces. Based on this semantics we develop a syntax of adeterministic version of the differential lambda-calculus. One nice feature ofthis new approach to differentiation is that it is compatible with generalfixpoints of terms, so our language is actually a differential extension of PCFfor which we provide a fully deterministic operational semantics