Resource Constrained Programming with Full Dependent Types

by Dr. Robert Atkey

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 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.

Bio

Bob Atkey is a Chancellor’s Fellow and Lecturer at the University of Strathclyde in Glasgow, Scotland. Before this position, he did a PhD and postdoc at the University of Edinburgh, and worked for a spin-out company on static analysis of concurrent Java programs.

School of Computer and Cyber Sciences Augusta University