A. Charguéraud, The Locally Nameless Representation, Journal of Automated Reasoning, vol.40, issue.12, pp.363-408, 2012.
DOI : 10.1007/s10817-008-9097-2

L. Chicli, L. Pottier, and C. Simpson, Mathematical Quotients and Quotient Types in Coq, Types for Proofs and Programs, pp.95-107, 2003.
DOI : 10.1007/3-540-39185-1_6

C. Cohen, Types quotients en coq, Actes des 21ème journées francophones des langages applicatifs, 2010.
DOI : 10.1007/978-3-642-39634-2_17

W. Ferrer and O. Malherbe, The category of implicative algebras and realizability. ArXiv e-prints, 2017.

W. Ferrer-santos, M. Guillermo, and O. Malherbe, Realizability in OCAs and AKSs. ArXiv e-prints, 2015.

J. Walter-ferrer-santos, M. Frey, O. Guillermo, A. Malherbe, and . Miquel, Ordered combinatory algebras and realizability, Mathematical Structures in Computer Science, vol.27, issue.03, pp.428-45810, 2017.
DOI : 10.1111/j.1746-8361.1969.tb01194.x

J. Frey, Realizability Toposes from Specifications, 13th International Conference on Typed Lambda Calculi and Applications of Leibniz International Proceedings in Informatics (LIPIcs), pp.196-210, 2015.

J. Frey, Classical Realizability in the CPS Target Language, The Thirtysecond Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXII). doi, pp.111-126, 2016.
DOI : 10.1016/j.entcs.2016.09.034

T. G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.47-58, 1990.
DOI : 10.1145/96709.96714

M. Hofmann, Extensional Concepts in Intensional Type Theory, 1995.

P. Hofstra and J. Van-oosten, Ordered partial combinatory algebras, Mathematical Proceedings of the Cambridge Philosophical Society, vol.134, issue.3, pp.445-46310, 2003.
DOI : 10.1017/S0305004102006424

J. Krivine, Realizability in classical logic In interactive models of computation and program behaviour, Panoramas et synthèses, vol.27, 2009.

J. Krivine, Realizability algebras: a program to well order R, Logical Methods in Computer Science, vol.40, issue.3, 2011.
DOI : 10.1007/s001530000057

URL : https://hal.archives-ouvertes.fr/hal-00483232

J. Krivine, Realizability algebras II : new models of ZF + DC, Logical Methods in Computer Science, vol.8, issue.1, p.10, 2012.
DOI : 10.1007/s001530000057

URL : https://hal.archives-ouvertes.fr/hal-00497587

J. Krivine, Quelques propriétés des modèles de réalisabilité de ZF, 2014.

A. Miquel, Existential witness extraction in classical realizability and via a negative translation, Logical Methods in Computer Science, vol.7, issue.2, pp.188-20210, 2011.
DOI : 10.1016/S0747-7171(89)80045-8

URL : https://hal.archives-ouvertes.fr/hal-00800560

A. Miquel, Implicative algebras Unpublished manuscript URL: https, 2018.

E. Miquey, Classical realizability and side-effects. Theses URL: https, 2017.
URL : https://hal.archives-ouvertes.fr/tel-01653733

G. Munch-maccagnoni, Focalisation and Classical Realisability, Computer Science Logic '09, pp.409-423, 2009.
DOI : 10.1016/0304-3975(87)90045-4

URL : https://hal.archives-ouvertes.fr/inria-00409793

A. M. Pitts, Tripos theory in retrospect, Mathematical Structures in Computer Science, vol.12, issue.3, pp.265-27910, 2002.

F. Ruyer and . Proofs, Types and Subtypes URL: https://tel.archives-ouvertes, p.140046, 2006.

M. Sozeau and N. Oury, First-Class Type Classes, Theorem Proving in Higher Order Logics, pp.278-293, 2008.
DOI : 10.1007/11542384_8

URL : https://hal.archives-ouvertes.fr/inria-00628864

T. Streicher, Krivine's classical realisability from a categorical perspective, Mathematical Structures in Computer Science, vol.27, issue.06, pp.1234-125610, 2013.
DOI : 10.1016/S0304-3975(02)00776-4