FSTTCS 2026

ALT In this paper, we show how a recently introduced λ-calculus for randomized computation, called λBLL, can accurately capture the notions of first- and second-order polytime computations used in cryptographic definitions and proofs. These results, spelled out in the style of so-called implicit computational complexity, imply that λBLL is sufficiently powerful to express experiments and adversaries as used in cryptography, and that reductions, when formulated within the calculus, are guaranteed to be complexity-preserving. Remarkably, while polynomial-time soundness holds for the full calculus, polynomial-time completeness already follows in presence of a minimal finite set of basic functions.