Applied Implicit Computational Complexity

Dissertation

• Compiled draft latest version
• Source code repository

Supplementary Documents

• Extended abstract
• Dissertation companion artifact
• License CC-BY-4.0

Abstract

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 systems drive better understanding of complexity classes, yield natural definitions and proofs, and produce techniques for automatable program analysis for free. However, despite the numerous advantages, ICC remains largely a theoretical novelty. This means the practical power, limitations, and advantages of ICC-based program 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 for analyzing resource usage. In other words, it allows to produce quantitative reports about programs execution behaviors in cases that are overlooked by other techniques. Second, it is possible to adjust the analyses to track other program properties. This suggests that unrealized potential is available in ICC systems, and we should learn to leverage it. The third finding is reflective and visionary. An essential feature of ICC is that it enables guaranteeing program properties by construction, before any program exists. This enables providing behavioral guarantees 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.