, Call-by-name, call-by-value, call-by-need and the linear lambda calculus, Theoretical Computer Science, vol.152, issue.2, p.330, 1995.

J. , but simpler and applicable to untyped ?-calculi. The underlying transition system has monadic values as states, and is essentially deterministic. This is indeed the reason the framework is only applicable to call-by-name (and not to call-by-value) calculi, in contrast with, Conclusion and Future Work We have shown how a notion of applicative similarity on call-by-name effectful lambda-calculi can be defined and proved fully-abstract, 2009.

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

S. Abramsky and A. Jung, Domain theory, Handbook of Logic in Computer Science, pp.1-168, 1994.

A. W. Appel and D. A. 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.

H. P. Barendregt and . H.b., Preface, The Lambda Calculus - Its Syntax and Semantics, pp.vii-viii, 1984.

N. Benton, A. Kennedy, L. Beringer, and M. Hofmann, Relational semantics for effect-based program transformations, Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming - PPDP '09, pp.301-312, 2009.

A. Bizjak and L. Birkedal, Step-Indexed Logical Relations for Probability, Lecture Notes in Computer Science, pp.279-294, 2015.

R. Crubillé and U. Dal-lago, On Probabilistic Applicative Bisimulation and Call-by-Value ?-Calculi, Programming Languages and Systems, vol.8410, pp.209-228, 2014.

U. Dal-lago, F. Gavazzo, and P. Levy, Effectful applicative bisimilarity: Monads, relators, and Howe's method (long version, 2017.

U. Dal-lago, D. Sangiorgi, and M. Alberti, On coinductive equivalences for higher-order probabilistic functional programs, ACM SIGPLAN Notices, vol.49, issue.1, pp.297-308, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01091573

B. A. Davey and H. A. Priestley, Introduction to Lattices and Order, 2002.

U. Deliguoro and A. Piperno, Nondeterministic Extensions of Untyped ?-Calculus, Information and Computation, vol.122, issue.2, pp.149-177, 1995.

P. Di-gianantonio, F. Honsell, and M. Lenisa, RPO, Second-order Contexts, and Lambda-calculus, Logical Methods in Computer Science, vol.5, issue.3, 2009.

A. D. Gordon, A Tutorial on Co-induction and Functional Programming, Functional Programming, Glasgow 1994, pp.78-95, 1995.

J. Goubault-larrecq, S. Lasota, and D. Nowak, Logical relations for monadic types, Mathematical Structures in Computer Science, vol.18, issue.06, p.1169, 2008.

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

P. Johann, A. Simpson, and J. Voigtländer, A Generic Operational Metatheory for Algebraic Effects, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.209-218, 2010.

C. Jones, Probabilistic non-determinism, 1990.

S. B. Lassen, Relational Reasoning about Contexts, BRICS Report Series, vol.4, issue.24, 1997.

S. Maclane, Categories for the Working Mathematician, 1971.

I. A. Mason and C. L. Talcott, Equivalence in functional languages with effects, Journal of Functional Programming, vol.1, issue.3, pp.287-327, 1991.

E. Moggi, Computational lambda-calculus and monads, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.14-23

J. Morris, Lambda calculus models of programming languages, 1969.

C. L. Ong, Non-determinism in a functional setting, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.275-286

A. M. Pitts, Howe's method for higher-order languages, Advanced Topics in Bisimulation and Coinduction, vol.52, pp.197-232

G. D. Plotkin and J. Power, Adequacy for Algebraic Effects, Lecture Notes in Computer Science, pp.1-24, 2001.

G. D. Plotkin and J. Power, Algebraic operations and generic effects, Applied Categorical Structures, vol.11, issue.1, pp.69-94, 2003.

M. O. Rabin and D. Scott, Finite Automata and Their Decision Problems, IBM Journal of Research and Development, vol.3, issue.2, pp.114-125, 1959.