The differential lambda-calculus: syntax and semantics for differential geometry
Date
2018-09-21
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
The differential λ-calculus was introduced to study the resource usage of programs. This thesis marks a change in that belief system; our thesis can be summarized by the analogy λ-calculus : functions ::∂λ-calculus : smooth functions. To accomplish this, we will describe a precise categorical semantics for the differential λ-calculus using categories with a differential operator. We will then describe explicit models that are relevant to differential geometry, using categories like Sikorski spaces and diffeological spaces.
Description
Keywords
differential geometry, linear logic, type theory, categorical logic, infinite dimension, convenient differential geometry, logic for differential geometry, logic-differential geometry correspondence
Citation
Gallagher, J. (2018). The differential lambda-calculus: syntax and semantics for differential geometry (Doctoral thesis, University of Calgary, Calgary, Canada). Retrieved from https://prism.ucalgary.ca. doi:10.11575/PRISM/33144