Mathematical Structures in Computer Science

Paper

Logical relations for monadic types

JEAN GOUBAULT-LARRECQa1, SŁAWOMIR LASOTAa2§ and DAVID NOWAKa3

a1 LSV, ENS Cachan, CNRS, INRIA

a2 Institute of Informatics, Warsaw University

a3 Research Center for Information Security, AIST

Abstract

Logical relations and their generalisations are a fundamental tool in proving properties of lambda calculi, for example, for yielding sound principles for observational equivalence. We propose a natural notion of logical relations that is able to deal with the monadic types of Moggi's computational lambda calculus. The treatment is categorical, and is based on notions of subsconing, mono factorisation systems and monad morphisms. Our approach has a number of interesting applications, including cases for lambda calculi with non-determinism (where being in a logical relation means being bisimilar), dynamic name creation and probabilistic systems.

(Received June 2004)

(Revised March 2008)

Footnotes

A preliminary version of this paper was presented at the 11th Annual Conference of the European Association for Computer Science Logic (CSL'02), Edinburgh, Scotland, 22–25 September 2002 (Goubault-Larrecq et al. 2002).

Work partially supported by the RNTL project EVA, and the ACI jeunes chercheurs ‘Sécurité informatique, protocoles cryptographiques et détection d'intrusions’.

§ Work partially supported by the Polish KBN grant 7 T11C 002 21, and the IST-2005-16004 Integrated Project SENSORIA: Software Engineering for Service-Oriented Overlay Computers.

Work partially supported by the ACI jeunes chercheurs ‘Sécurité informatique, protocoles cryptographiques et détection d'intrusions’.