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

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. ,

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

Domain theory, Handbook of Logic in Computer Science, pp.1-168, 1994. ,

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. ,

Preface, The Lambda Calculus - Its Syntax and Semantics, pp.vii-viii, 1984. ,

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. ,

Step-Indexed Logical Relations for Probability, Lecture Notes in Computer Science, pp.279-294, 2015. ,

On Probabilistic Applicative Bisimulation and Call-by-Value ?-Calculi, Programming Languages and Systems, vol.8410, pp.209-228, 2014. ,

Effectful applicative bisimilarity: Monads, relators, and Howe's method (long version, 2017. ,

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

Introduction to Lattices and Order, 2002. ,

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

RPO, Second-order Contexts, and Lambda-calculus, Logical Methods in Computer Science, vol.5, issue.3, 2009. ,

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

Logical relations for monadic types, Mathematical Structures in Computer Science, vol.18, issue.06, p.1169, 2008. ,

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

A Generic Operational Metatheory for Algebraic Effects, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.209-218, 2010. ,

Probabilistic non-determinism, 1990. ,

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

Categories for the Working Mathematician, 1971. ,

Equivalence in functional languages with effects, Journal of Functional Programming, vol.1, issue.3, pp.287-327, 1991. ,

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

Lambda calculus models of programming languages, 1969. ,

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

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

Adequacy for Algebraic Effects, Lecture Notes in Computer Science, pp.1-24, 2001. ,

Algebraic operations and generic effects, Applied Categorical Structures, vol.11, issue.1, pp.69-94, 2003. ,

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