Z. M. Ariola, P. Downen, H. Herbelin, K. Nakata, and A. Saurin, Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts, pp.32-46, 2012.
DOI : 10.1007/978-3-642-29822-6_6
URL : https://hal.archives-ouvertes.fr/hal-00697241

S. Berardi, M. Bezem, and T. Coquand, Abstract, The Journal of Symbolic Logic, vol.39, issue.02, pp.600-622, 1998.
DOI : 10.1007/BF02007566

U. Berger and P. Oliva, Modified bar recursion, Mathematical Structures in Computer Science, vol.16, issue.02, pp.163-183, 2006.
DOI : 10.1017/S0960129506005093

P. Curien and H. Herbelin, The duality of computation, pp.233-243, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

H. Martín, P. Escardó, and . Oliva, Bar recursion and products of selection functions, CoRR abs, p.7046, 1407.

H. Herbelin, A constructive proof of dependent choice, compatible with classical logic, Logic in Computer Science, LICS Proceedings, IEEE Computer Society, vol.2012, pp.365-374, 2012.