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
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.