Cockett, J. Robin B.Gallagher, Jonathan2018-10-092018-10-092018-09-21http://hdl.handle.net/1880/108793The 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.engUniversity of Calgary graduate students retain copyright ownership and moral rights for their thesis. You may use this material in any way that is permitted by the Copyright Act or through licensing that has been assigned to the document. For uses that are not allowable under copyright legislation or licensing, you are required to seek permission.differential geometrylinear logictype theorycategorical logicinfinite dimensionconvenient differential geometrylogic for differential geometrylogic-differential geometry correspondenceEducation--MathematicsEducation--SciencesEducation--TechnologyPhysicsPhysics--TheoryApplied SciencesComputer Sciencedoctoral thesis10.11575/PRISM/33144