S. Abramsky, The lazy lambda calculus, Research Topics in Functional Programming, pp.65-117, 1990.

A. Cappai and U. D. Lago, On equivalences, metrics, and polynomial time (long version), 2015.

R. Crubillé and U. D. Lago, On Probabilistic Applicative Bisimulation and Call-by-Value ??-Calculi, ESOP, pp.209-228, 2014.
DOI : 10.1007/978-3-642-54833-8_12

U. Dal-lago, D. Sangiorgi, and M. Alberti, On coinductive equivalences for higher-order probabilistic functional programs, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, 2014.
DOI : 10.1145/2535838.2535872

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

U. Dal, L. , and P. Parisen-toldin, A higher-order characterization of probabilistic polynomial time, FOPARA, pp.1-18, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01231752

U. Dal-lago, S. Zuppiroli, and M. Gabbrielli, Probabilistic recursion theory and implicit computational complexity, Sci. Ann. Comp. Sci, vol.24, issue.2, pp.177-216, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01091595

Y. Deng and Y. Zhang, Program equivalence in linear contexts. CoRR, abs, 1106.

J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden, Metrics for Labeled Markov Systems, In CONCUR LNCS, vol.1664, pp.258-273, 1999.
DOI : 10.1007/3-540-48320-9_19

O. Goldreich, The Foundations of Cryptography -Volume 1, Basic Techniques, 2001.

O. Goldreich and M. Sudan, Computational indistinguishability: a sample hierarchy, Proceedings. Thirteenth Annual IEEE Conference on Computational Complexity (Formerly: Structure in Complexity Theory Conference) (Cat. No.98CB36247), pp.24-33, 1998.
DOI : 10.1109/CCC.1998.694588

M. Hofmann, A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion, CSL, pp.275-294, 1997.
DOI : 10.1007/BFb0028020

M. Hofmann, Safe recursion with higher types and BCK-algebra, Annals of Pure and Applied Logic, vol.104, issue.1-3, pp.113-166, 2000.
DOI : 10.1016/S0168-0072(00)00010-5

URL : http://doi.org/10.1016/s0168-0072(00)00010-5

D. J. Howe, Proving Congruence of Bisimulation in Functional Programming Languages, Information and Computation, vol.124, issue.2, pp.103-112, 1996.
DOI : 10.1006/inco.1996.0008

J. Katz and Y. Lindell, Introduction to Modern Cryptography. Chapman and Hall, 2007.

J. C. Mitchell, M. Mitchell, and A. Scedrov, A linguistic characterization of bounded oracle computation and probabilistic polynomial time, Proceedings 39th Annual Symposium on Foundations of Computer Science (Cat. No.98CB36280), pp.725-733, 1998.
DOI : 10.1109/SFCS.1998.743523

D. Nowak and Y. Zhang, A Calculus for Game-Based Security Proofs, PROVSEC, pp.35-52, 2010.
DOI : 10.1007/978-3-642-02273-9_29

Y. Zhang, The computational SLR: a logic for reasoning about computational indistinguishability, Mathematical Structures in Computer Science, vol.4861, issue.05, pp.951-975, 2010.
DOI : 10.1007/BF01201998