Bisimulation in Untyped Lambda Calculus:

Abramsky, 1990, The lazy lambda calculus, 65 Abramsky, 1993, Full abstraction in the lazy lambda calculus, Information and Computation, 105, 159, 10.1006/inco.1993.1044 Barendregt, 1984, The Lambda Calculus: Its Syntax and Semantics, 10.1016/S0049-237X(08)71818-4 G. Berry, “Modèles complètement adéquats et stables des lambda calculus typés,” Thèse de doctorat d'etat, Université Paris VII, 1979. G. Boudol, On the semantics of the call-by-name CPS transform, Theoretical Computer Science, 1999, Note, To appear. David, 1997, A syntactical proof of the operational equivalence of two λ-terms, Theoretical Computer Science, 180, 371, 10.1016/S0304-3975(97)00004-2 M. Dezani-Ciancaglini, J. Tiuryn, and P. Urzyczyn, Discrimination by parallel observers, In: Proc. 12th Annual IEEE Symposium on Logic in Computer Science, 1997, pages 396–407. H. Goguen, Soundness of typed operational semantics for the logical framework, In: Proc. 4th International Conference on Typed Lambda Calculus and Applications, L'Aquila, Italy, Lecture Notes in Computer Science 1581 (1999), Springer-Verlag. A. D. Gordon, Bisimilarity as a theory of functional programming, In: Proc. 11th Conference of Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science 1 (1995), URL: http://www.elsevier.nl/locate/entcs/volume1.html. 1998 F. Honsell and M. Lenisa, Final semantics for untyped lambda-calculus, In: Proc. 2nd International Conference on Typed Lambda Calculus and Applications, Edinburgh, Lecture Notes in Computer Science 902 (1995), pp. 249–265. Howe, 1996, Proving congruence of bisimulation in functional programming languages, Information and Computation, 124, 103, 10.1006/inco.1996.0008 Hyland, 1976, A Syntactic characterisation of the equality in some models for the lambda calculus, Journal of the London Mathematical Society, 12, 361, 10.1112/jlms/s2-12.3.361 Jacobs, 1997, A tutorial on (co)algebras and (co)induction, Bulletin of the EATCS, 62, 222 S. B. Lassen, Relational reasoning about contexts, In: Gordon and Pitts [10], pages 91–135. M. Lenisa, A uniform syntactical method for proving coinduction principles in λ-calculi, In: M. Bidoit and M. Dauchet, editors, TAPSOFT '97, Lecture Notes in Computer Science 1214 (1997), pp. 309–320. Longo, 1983, Set-theoretical models of lambda calculus: Theories, expansions and isomophisms, Annals of Pure and Applied Logic, 24, 153, 10.1016/0168-0072(83)90030-1 J. H. Morris, “Lambda-Calculus Models of Programming Languages,” PhD thesis, MIT, Dec. 1968. C.-H. L. Ong, “The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming,” PhD thesis, University of London, 1988. D. Sands, Improvement theory and its applications, In Gordon and Pitts [10], pages 275–306. Sangiorgi, 1994, The lazy lambda calculus in a concurrency senario, Information and Computation, 111, 120, 10.1006/inco.1994.1042 D. Sangiorgi, On the bisimulation proof method, Technical Report LFCS-94-299, University of Edinburgh, Aug. 1994. Wadsworth, 1976, The relation between computational and denotational properties for Scott's D∞-models of the lambda-calculus, SIAM Journal on Computing, 5, 488, 10.1137/0205036