What is a categorical model of the differential and the resource lambda-calculi?
Manzonetto Giulio (CS)
TL;DR
This paper develops an abstract model theory for the untyped differential and resource lambda-calculi using linear reflexive objects in Cartesian closed differential categories, with relation-based examples.
Contribution
It introduces a general definition of models for these calculi, expanding the theoretical understanding of their semantic foundations.
Findings
Proposes a new model framework for differential and resource lambda-calculi.
Provides concrete examples of models based on relations.
Establishes the notion of linear reflexive objects in differential categories.
Abstract
In this paper we provide an abstract model theory for the untyped differential lambda-calculus and the resource calculus. In particular we propose a general definition of model of these calculi, namely the notion of linear reflexive object in a Cartesian closed differential category. Examples of models based on relations are provided.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Advanced Database Systems and Queries