2020/11/30 by Mario Alvarez-Picallo, Alvarez-Picallo, Mario, C.-H. Luke Ong +1
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2011.14476
openalex publication_date 2020/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.