Abstract
In his lecture, François Pottier showed that a program logic can not only establish the correctness of a program, but also control the number of operations it performs, and therefore, indirectly, its computation time.
He explained how this counting can be done first in Hoare logic, then in separation logic, where time counting can be carried out in a more decentralized way, and very elaborate accounting tricks can be set up by the user.
