  Cartesian difference categories are a recent generalisation of Cartesian
differential categories which introduce a notion of "infinitesimal" arrows
satisfying an analogue of the Kock-Lawvere axiom, with the axioms of a
Cartesian differential category being satisfied only "up to an infinitesimal
perturbation". In this work, we construct a simply-typed calculus in the spirit
of the differential lambda-calculus equipped with syntactic infinitesimals and
show how its models correspond to difference lambda-categories, a family of
Cartesian difference categories equipped with suitably well-behaved
exponentials.
