Neea Rusch

Certifying Complexity Analysis

I presented this talk at CoqPL'23 in Boston, on January 21, 2023.


This work drafts a strategy that leverages the field of Implicit Computational Complexity to certify resource usage in imperative programs. This original approach sidesteps some of the most common–and difficult–obstacles “traditional” complexity theory face when implemented in Coq.