Categorical models of the differential λ-calculus

The paper shows how the Scott-Koymans theorem for the untyped lambda-calculus can be extended to the differential lambda-calculus. The main result is that every model of the untyped differential lambda-calculus may be viewed as a differential reflexive object in a Cartesian-closed differential category. This extension of the Scott-Koymans theorem depends critically on unraveling the somewhat subtle issue of which idempotents can be split so that differential structure lifts to the idempotent splitting. The paper uses (total) Turing categories with "canonical codes" as the basic categorical semantics for the lambda-calculus. It develops the main result in a modular fashion by showing how to add left-additive structure to a Turing category, and then - on top of that - differential structure. For both levels of structure, it is necessary to identify how "canonical codes" must behave with respect to the added structure and, furthermore, how "universal objects" must behave. The latter is closely tied to the question - which is the crux of the paper - of which idempotents can be split while preserving the differential structure of the setting. This paper is the full version of a conference paper and includes the proofs which were omitted from that version due to page-length restrictions.