Herman Geuvers (2014):
A typed λ-calculus with CBN and CBV iterators.
To appear.
J.M. Jansen (2013):
Programming in the λ-Calculus: From Church to Scott and Back.
In: The Beauty of Functional Code,
Lecture Notes in Computer Science 8106,
pp. 168–180,
doi:10.1007/978-3-642-38143-0.
Jean-Louis Krivine (1994):
Classical Logic, Storage Operators and Second-Order lambda-Calculus.
Ann. Pure Appl. Logic 68(1),
pp. 53–78,
doi:10.1016/0168-0072(94)90047-7.
A. Miquel (2009):
Classical realizability with forcing and the axiom of countable choice.
http://perso.ens-lyon.fr/alexandre.miquel/habilitation/forcing.pdf.