A. Ahmed, Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types, Proceedings of ESOP, 2006.
DOI : 10.1017/S0956796800000125
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.3992

A. Ahmed, D. Dreyer, and A. Rossberg, State-dependent Representation Independence, Proceedings of POPL, 2009.
DOI : 10.1145/1480881.1480925

A. J. Ahmed, Semantics of Types for Mutable State, 2004.

A. W. Appel, R. Dockins, A. Hobor, J. Dodds, X. Leroy et al., Program Logics for Certified Compilers, 2014.
DOI : 10.1017/CBO9781107256552

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

A. W. Appel, P. Mellì-es, C. D. Richards, and J. Vouillon, A Very Modal Model of a Modern, Major, General Type System, Proceedings of POPL, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00150978

N. Benton, C. Hur, and . Biorthogonality, Step-Indexing and Compiler Correctness, Proceedings of ICFP, 2009.
DOI : 10.1145/1596550.1596567

L. Birkedal, A. Bizjak, and J. Schwinghammer, Step-Indexed Relational Reasoning for Countable Nondeterminism, Logical Methods in Computer Science, vol.9, issue.4, pp.1-23, 2013.
DOI : 10.2168/LMCS-9(4:4)2013
URL : http://arxiv.org/abs/1310.2031

L. Birkedal, R. E. Møgelberg, J. Schwinghammer, and K. Støvring, First steps in synthetic guarded domain theory: step-indexing in the topos of trees, Logical Methods in Computer Science, vol.8, issue.4, p.2012

L. Birkedal, B. Reus, J. Schwinghammer, K. Støvring, J. Thamsborg et al., Step-Indexed Kripke Models over Recursive Worlds, Proceedings of POPL, 2011.
DOI : 10.1145/1925844.1926401
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.190.2081

L. Birkedal, F. Sieczkowski, and J. Thamsborg, A Concurrent Logical Relation, Proceedings of CSL, 2012.

L. Birkedal, K. Støvring, and J. Thamsborg, The category-theoretic solution of recursive metric-space equations, Theoretical Computer Science, vol.411, issue.47, pp.4102-4122, 2010.
DOI : 10.1016/j.tcs.2010.07.010

D. Gianantonio and M. Miculan, A Unifying Approach to Recursive and Corecursive Definitions, Proceedings of TYPES, 2002.

M. Dodds, S. Jagannathan, M. Parkinson, K. Svendsen, and L. Birkedal, Verifying Custom Synchronisation Constructs Using Higher-Order Separation Logic
DOI : 10.1145/2818638

D. Dreyer, G. Neis, and L. Birkedal, The impact of higher-order state and control effects on local relational reasoning, Journal of Functional Programming, vol.69, issue.4-5, pp.477-528, 2012.
DOI : 10.1145/1889997.1890002

A. Hobor, R. Dockins, and A. W. Appel, A Theory of Indirection via Approximation, Proceedings of POPL, 2010.

C. Hur and D. Dreyer, A Kripke Logical Relation Between ML and Assembly, Proceedings of POPL, 2011.
DOI : 10.1145/1925844.1926402
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.170.3013

R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon et al., Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning, Proceedings of POPL, 2015.

J. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, 2002.
DOI : 10.1109/LICS.2002.1029817

K. Svendsen and L. Birkedal, Impredicative Concurrent Abstract Predicates, Proceedings of ESOP, 2014.
DOI : 10.1007/978-3-642-54833-8_9

A. Turon, D. Dreyer, and L. Birkedal, Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency, Proceedings of ICFP, 2013.

A. J. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, and D. Dreyer, Logical Relations for Fine-grained Concurrency, Proceedings of POPL, 2013.
DOI : 10.1145/2429069.2429111