Abstract. Software is vital for modern society: it manages finances, regulates power generation and communications, controls airplanes, and processes security-critical information. Thus the development of formal methods to verify the correctness and reliability of programs is of crucial importance, in particular in contexts where the amount of resources can be used during the execution of a program is limited (e.g., small computational devices like pacemakers, PDA's or intelligent phones).

In this project, the researchers will develop a denotational semantics for the differential λ-calculus, a new programming language designed for having a major control on the execution of programs running on bounded resources environments. Denotational semantics aims to represent the meaning of programming languages through mathematical objects called "models". The researchers will then build models of differential λ-calculus and analyze them by applying a mixture of techniques originating in the context of universal algebra, category theory and topology.

The proposed researches are incremental: the researchers will first focus on denotational models of λ-calculus, a paradigmatic programming language constituting the kernel of differential λ-calculus, and will subsequently extend their results to the more complex framework of differential λ-calculus.
The resulting outcomes are expected to benefit the community of logicians and computer scientists working on the verification and design of programming languages, as well as the community of algebraists.