Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs

We define a call-by-value variant of Godel's system T with references, and equip it with a linear dependent type and effect system, called dlT, that can estimate the time complexity of programs, as a function of the size of their inputs. We prove that the type system is intentionally sound, in the sense that it over-approximates the complexity of executing the programs on a variant of the CEK abstract machine. Moreover, we define a sound and complete type inference algorithm which critically exploits the subrecursive nature of dlT. Finally, we demonstrate the usefulness of dlT for analyzing the complexity of cryptographic reductions by providing an upper bound for the constructed adversary of the Goldreich-Levin theorem.