Fresh Perspectives on Implicit Computational Complexity

Implicit computational complexity (ICC) complements classic complexity theory by developing machine-independent characterizations of complexity classes. The idea is to introduce a restriction, at the level of a programming language, that guarantees every program satisfying the restriction belongs to a particular complexity class. There are several good motivations for the ICC approach: it drives better understanding of complexity classes, yields natural definitions and proofs, and produces automatable program analysis techniques for free. However, despite the numerous advantages, ICC remains largely a theoretical novelty. Therefore, the true power and advantages of ICC-based analyses are not well-understood. This talk explores how to "put ICC theories to test" by investigating their capabilities outside the theoretical domain. A guiding intuition is that, if applied, implicit computational complexity could provide us new and orthogonal techniques for program analysis and verification.