Slides and Video for “Resource Constrained Programming with Full Dependent Types”
Last Friday, I gave a talk (virtually) at the CCS Colloquim at Augusta University, hosted by Harley Eades III. The title was “Resource Constrained Programming with Full Dependent Types” and the abstract was:
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 linear and polynomial time computation to full dependent types. This results in a system where unconstrained computations are permitted at the type level, but only polynominal time computations are permitted at the term level. The combined system now allows one to explore the world of propositions whose proofs are not only constructive, but also of restricted complexity.
The talk was recorded, and the video is on YouTube. The slides:
