Slides for “Resource Constrained Programming with Full Dependent Types”
Yesterday, I gave a talk entitled “Resource Constrained Programming with Full Dependent Types” at the IRIF Proofs, Programs and systems seminar in Paris. Many thanks to Paul-André Melliès for inviting me to give a talk.
Abstract:
I will talk about a system that combines Dependent Types and Linear Types. As an application of this system, I will show how to transport Martin Hofmann's LFPL and Amortised Resource analysis systems for resource constrained computing to full dependent types. This results in a theory where unconstrained computations are allowed at the type level, but only polynomial time computations at the term level. The combined system allows one to explore the world of propositions whose proofs are not only constructive, but also of restricted complexity.
Slides:
