Applied 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 strong motivations for this approach, including that ICC 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. The true power and advantages of ICC-based analyses are not well-understood. The dissertation research "puts 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 techniques for program analysis and verification. Over a series of projects, the dissertation work yields three main findings. The first shows that ICC offers complementary techniques to automatic resource analysis. Second, it is possible to adjust ICC systems to track other program properties. This suggests unrealized potential is available in ICC systems and we should learn to leverage it. The final finding is a reflective and visionary. A core aspect of ICC is that it enables guaranteeing program properties by construction, before any program exists. This means we can ensure correct behavior without needing to run any post-analysis. This is a powerful concept in principle, but still beyond reach. The practical attainability of this goal depends crucially on a viewpoint shift—we should consider ICC in the broader context it offers and continue exploring its applied potential.