| In this project we will develop algebraic and categorical tools for studying the denotational semantics of the differential lambda calculus. This calculus is a recent paradigmatic functional programming language enriched with a syntactic derivative operator permitting a major control on the amount of resources used by a program. Our main goals are to formalize abstract notions of a model of the differential lambda calculus, to study concrete examples of models of this calculus arisen from the relational semantics of linear logic, and to provide general set-theoretical constructions to build classes of such models. To achieve these goals we will first focus on the models of the pure untyped lambda calculus, which constitutes the kernel of all functional programming languages and, in particular, of the differential lambda calculus. Combining techniques of universal algebra and category theory which emerged in Manzonetto's previous work, we expect to: (i) propose a more general notion of model of lambda calculus allowing to build an equationally complete semantics; (ii) provide a categorical road-map of the current notions of models of computations clarifying the relationships among them; (iii) prove representation theorems for models of computations, in order to provide a taxonomy for the different notions of computability; (iv) develop a natural duality theory for denotational models to apply powerful topological methods on such algebraic structures. These results will be then generalized to the models of the differential lambda calculus. |
