We define a call-by-value variant of G¨odel’s System T with references, and equip it with a linear dependent type and effect system, called dlT, that can estimate the 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.
Baillot, P., Barthe, G., Dal Lago, U. (2015). Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs. Springer Verlag [10.1007/978-3-662-48899-7_15].
Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
DAL LAGO, UGO
2015
Abstract
We define a call-by-value variant of G¨odel’s System T with references, and equip it with a linear dependent type and effect system, called dlT, that can estimate the 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.