A. Ahmed, Step-indexed syntactic logical relations for recursive and quantified types. Programming Languages and Systems, pp.69-83, 2006.
DOI : 10.1007/11693024_6

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

A. W. Appel and D. Mcallester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems, vol.23, issue.5, pp.657-683, 2001.
DOI : 10.1145/504709.504712

N. Benton and C. Hur, Step-indexing: the good, the bad and the ugly, Proceedings of Dagstuhl Seminar 10351: Modelling, Controlling and Reasoning About State

N. Benton and C. Hur, Biorthogonality, step-indexing and compiler correctness, ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming, pp.97-108, 2009.
DOI : 10.1145/1596550.1596567

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

N. Benton and N. Tabareau, Compiling functional types to relational specifications for low level imperative code, Proceedings of the 4th international workshop on Types in language design and implementation, TLDI '09, pp.3-14, 2009.
DOI : 10.1145/1481861.1481864

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

C. Hur and D. Dreyer, A Kripke logical relation between ML and assembly, POPL '11: Proceedings of the 38th ACM Symposium on Principles of Programming Languages, pp.133-146, 2011.
DOI : 10.1145/1925844.1926402

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

G. Jaber and N. Tabareau, Krivine realizability for compiler correctness, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00475210

G. Jaber and N. Tabareau, Decomposing Logical Relations with Forcing, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00585717

A. Nanevski, G. Morrisett, and L. Birkedal, Polymorphism and Separation in Hoare Type Theory, ICFP '06: Proceedings of the eleventh ACM SIGPLAN International Conference on Functional Programming, p.73, 2006.

A. M. Pitts and I. D. Stark, Operational reasoning for functions with local state, Higher Order Operational Techniques in Semantics. CUP, 1998.