Conference item
The difference λ-calculus: a language for difference categories
- Abstract:
- 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 λ-calculus equipped with syntactic "infinitesimals" and show how its models correspond to difference λ-categories, a family of Cartesian difference categories equipped with suitably well-behaved exponentials.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Version of record, pdf, 590.2KB, Terms of use)
-
- Publisher copy:
- 10.4230/LIPIcs.FSCD.2020.32
Authors
- Publisher:
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik
- Host title:
- Leibniz International Proceedings in Informatics, LIPIcs
- Journal:
- LIPIcs More from this journal
- Volume:
- 167
- Pages:
- 32:1–32:21
- Article number:
- 32
- Publication date:
- 2020-06-01
- Event title:
- 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
- DOI:
- ISSN:
-
1868-8969
- ISBN:
- 9783959771559
- Language:
-
English
- Keywords:
- Pubs id:
-
1127671
- Local pid:
-
pubs:1127671
- Deposit date:
-
2021-03-08
- ARK identifier:
Terms of use
- Copyright holder:
- Mario Alvarez-Picallo and C.-H. Luke Ong
- Copyright date:
- 2020
- Rights statement:
- ©2020 Mario Alvarez-Picallo and C.-H. Luke Ong; licensed under Creative Commons License CC-BY
- Licence:
- CC Attribution (CC BY)
If you are the owner of this record, you can report an update to it here: Report update to this record