The differential lambda-calculus: syntax and semantics for differential geometry

Thumbnail Image

Files

ucalgary_2018_gallagher_jonathan.pdf (1.06 MB)

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

URI

http://hdl.handle.net/1880/108793

Collections

Open Theses and Dissertations

Endorsement

Review

Supplemented By

Referenced By

Powered by

Libraries & Cultural Resources

Start Something.

University of Calgary
2500 University Drive NW
Calgary Alberta T2N 1N4
CANADA

Copyright © 2023

The University of Calgary, located in the heart of Southern Alberta, both acknowledges and pays tribute to the traditional territories of the peoples of Treaty 7, which include the Blackfoot Confederacy (comprised of the Siksika, the Piikani, and the Kainai First Nations), the Tsuut’ina First Nation, and the Stoney Nakoda (including Chiniki, Bearspaw, and Goodstoney First Nations). The City of Calgary is also home to the Métis Nation of Alberta (Districts 5 and 6).

The University of Calgary is situated on land Northwest of where the Bow River meets the Elbow River, a site traditionally known as Moh’kins’tsis to the Blackfoot, Wîchîspa to the Stoney Nakoda, and Guts’ists’i to the Tsuut’ina. On this land and in this place we strive to learn together, walk together, and grow together “in a good way.”