Marco Gaboardi (Università di Bologna)

Linear Dependent Types for Certified Resource Consumption

http://www.cs.unibo.it/~gaboardi

Resumé: I present the ideas underlying the design of an interactive programming framework useful to ensure the reliability and correctness of programs with respect to their resource consumption.

The key ingredient of this framework is a type system, dlPCF, mixing ideas from linear logic and dependent types. I introduce dlPCF and I show that it is sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely capture the functional behaviour of programs (i.e. how the output relates to the input) but also some of their intensional properties, namely the complexity of their evaluation. Additionally, dlPCF is parametrized on the underlying language of index terms, which can be tuned so as to sacrifice completeness for tractability.

Finally, I will show a possible use of dlPCF combined with Krivine's Realizability in the setting of cost-preserving certified compilation.