Strong Call-by-Value is Reasonable, Implosively

Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen

Whether the number of beta-steps in the lambda-calculus can be taken as a reasonable time cost model (that is, polynomially related to the one of Turing machines) is a delicate pro…