Logical relations andt heir generalizations are a fundamental tool in proving properties of lambda-calculi, e.g., yielding sound principles for observational equivalence. We propose a natural notion of logical relations able to deal with the monadic types of Moggi’s computational lambda-calculus. The treatment is categorical, and is based on notions of subsconing and distributivity laws for monads. Our approach has a number of interesting applications, including cases for lambda-calculi with non-determinism (where being in logical relation means being bisimilar), dynamic name creation, and probabilistic systems.
CITATION STYLE
Goubault-Larrecq, J., Lasota, S., & Nowak, D. (2002). Logical relations for monadic types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2471, pp. 553–568). Springer Verlag. https://doi.org/10.1007/3-540-45793-3_37
Mendeley helps you to discover research relevant for your work.