A call-by-value lambda-calculus with lists and control

Robbert Krebbers

Calculi with control operators have been studied to reason about control in programming languages and to interpret the computational content of classical proofs. To make these calc…