A. Abel, Normalization by Evaluation: Dependent Types and Impredicativity, 2013.

A. Abel and G. Scherer, On Irrelevance and Algorithmic Equality in Predicative Type Theory, Logical Methods in Computer Science, vol.8, issue.1, p.2012
DOI : 10.2168/LMCS-8(1:29)2012

R. Atkey, N. Ghani, and P. Johann, A relationally parametric model of dependent type theory, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.503-516, 2014.
DOI : 10.1145/2535838.2535852

J. Bernardy and M. Lasson, Realizability and Parametricity in Pure Type Systems, Foundations of Software Science and Computational Structures -14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011. Proceedings, pp.108-122, 2011.
DOI : 10.1007/978-3-642-19805-2_8

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

P. Curien and H. Herbelin, The duality of computation, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pp.233-243, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

H. Herbelin, C'est maintenant qu'on calcule, 2011.

D. Ilik, Continuation-passing style models complete for intuitionistic logic, Annals of Pure and Applied Logic, vol.164, issue.6, pp.651-662, 2013.
DOI : 10.1016/j.apal.2012.05.003

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

G. Munch-maccagnoni, Focalisation and Classical Realisability (version with appendices), 18th EACSL Annual Conference on Computer Science Logic - CSL 09, pp.409-423, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00409793

G. Munch-maccagnoni, Syntax and Models of a Non-Associative Composition of Programs and Proofs, 2013.
URL : https://hal.archives-ouvertes.fr/tel-00918642

P. Oliva and T. Streicher, On krivine's realizability interpretation of classical second-order arithmetic, Fundam. Inform, vol.84, issue.2, pp.207-220, 2008.

A. M. Pitts, Operational semantics and program equivalence Advanced Lectures, Applied Semantics, International Summer School, pp.378-412, 2000.
DOI : 10.1007/3-540-45699-6_8

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

A. J. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, and D. Dreyer, Logical relations for finegrained concurrency, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pp.343-356, 2013.