"A Dependently Typed Framework for Static Analysis of Program Execution Costs."

Edwin C. Brady, Kevin Hammond (2005)
a service of Schloss Dagstuhl - Leibniz Center for Informatics