On Equivalences, Metrics, and Polynomial Time (Long Version)

Alberto Cappai, Ugo Dal Lago

Interactive behaviors are ubiquitous in modern cryptography, but are also present in $\lambda$-calculi, in the form of higher-order constructions. Traditionally, however, typed $\lambda$-calcu…