It happens to every one of us to see a program “freeze”, and we may sometimes notice that a program occupy more memory that what we actually had available. While those are minor downsides in most of our daily usage, it can lead to dramatic consequences when human lives, security, or spatial exploration are at stakes. Most procedures test programs once they have been written and compiled, and provide an a posteriori seal that the program will behave according to its specification. My research area designs programming languages that can only produce “pre-certified” programs, i.e., programs that already come with that seal. The a posteriori test was replaced by the mathematical theorem guaranteeing that the program will end within pre-computed bounds on memory and time.
In this talk, I will sketch the goals and benefits of this approach, called Implicit Computational Complexity. One of my contribution was to identify simple principles in logic programs that can guarantee bounds on time or space. It uses proof-, automata-, and type-theory, a bit of complexity, but reached a stage of maturity that allow to express those results in simple terms, and to develop fascinating perspectives.
Monday, February 6, 2017, 2:30 PM – 3:30 PM
Appalachian State University, Anne Belk Hall, Room 318
All my publications are available at https://lacl.fr/~caubert/#publications, at arXiv and at HAL.
pdf version or the md source of this page