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.

Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs

Dal Lago U.
2019

Abstract

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.
2019
Baillot P.; Barthe G.; Dal Lago U.
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/732589
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact