Logics and Type Systems for Computational Complexity

Indiana University, Bloomington IN

Investigators

Abstract

The certitude that software execution terminates in principle is of little use without a grasp of the resources required, in particular computation time and space as functions of input size. Research over the last decade has demonstrated the potential of implicit static analysis of computational complexity, that is, programming and verification paradigms that automatically guarantee program execution within feasible resources, without an explicit analysis of algorithmic complexity in terms of machine models. This project further explores the conceptual underpinnings of machine-independent complexity, in particular abstraction mechanisms in functional programs and verification systems. It studies the implementation of these principles within major programming paradigms and styles, notably declarative and object oriented programming. Finally, it initiates applications of implicit complexity in Feasible Mathematics, in the guise of a library of formal proofs which establish the feasible computational contents of mathematical theorems without referring explicitly to computational complexity.