Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs

We define a call-by-value variant of Gödel’s system T with references, and equip it with a linear dependent type and effect system, called dℓT, 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 dℓT. Finally, we demonstrate the usefulness of dℓT for analyzing the complexity of cryptographic reductions by providing an upper bound for the constructed adversary of the Goldreich–Levin theorem.