Hostname: page-component-8448b6f56d-m8qmq Total loading time: 0 Render date: 2024-04-19T20:14:25.418Z Has data issue: false hasContentIssue false
  • English
  • Français

Logical relations for monadic types†

Published online by Cambridge University Press:  01 December 2008

JEAN GOUBAULT-LARRECQ ,
SŁAWOMIR LASOTA  and
DAVID NOWAK
JEAN GOUBAULT-LARRECQ
Affiliation:
LSV, ENS Cachan, CNRS, INRIA
SŁAWOMIR LASOTA
Affiliation:
Institute of Informatics, Warsaw University
DAVID NOWAK
Affiliation:
Research Center for Information Security, AIST
Get access Rights & Permissions [Opens in a new window]

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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 18 , Issue 6 , December 2008 , pp. 1169 - 1217
Copyright
Copyright © Cambridge University Press 2008

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abramsky, S. and Jung, A. (1994) Domain theory. In: Abramsky, S., Gabbay, D. M. and Maibaum, T. S. E. (eds.) Handbook of Logic in Computer Science, volume 3, Oxford University Press 1–168.Google Scholar
Adamek, J., Herrlich, H. and Strecker, G. (1990) Abstract and Concrete Categories, Wiley.Google Scholar
Alimohamed, M. (1995) A characterization of lambda definability in categorical models of implicit polymorphism. Theoretical Computer Science 146 (1-2)5–23.CrossRefGoogle Scholar
Ambler, S. J. (1991) First Order Linear Logic in Symmetric Monoidal Closed Categories, Ph.D. thesis, University of Edinburgh.Google Scholar
Appelgate, H. (1965) Acyclic models and resolvent functors, Ph.D. thesis, Columbia University.Google Scholar
Barr, M. (1998) The separated extensional Chu category. Theory and Applications of Categories 4 (6)137–147.Google Scholar
Beck, J. (1969) Distributive laws. In: Seminar on Triples and Categorical Homology Theory. Springer-Verlag Lecture Notes in Mathematics 80 119–140.CrossRefGoogle Scholar
Carboni, A., Kelly, G. M. and Wood, R. J. (1990) A 2-categorical approach to change of base and geometric morphisms I. Report 90-1, Department of Pure Mathematics, University of Sydney.Google Scholar
Crole, R. and Pitts, A. (1992) New foundations for fixpoint computations: Fix-hyperdoctrines and the fix-logic. Information and Computation 98 171–210.CrossRefGoogle Scholar
Eilenberg, S. and Kelly, G. M. (1966) Closed categories. In: Proceedings of the Conference on Categorical Algebra at La Jolla, Springer-Verlag 421–562.CrossRefGoogle Scholar
Fiore, M. and Simpson, A. (1999) Lambda definability with sums via Grothendieck logical relations. In: Proceedings of the 4th International Conference on Typed Lambda-Calculi and Applications (TLCA'99). Springer-Verlag Lecture Notes in Computer Science 1581 147–161.CrossRefGoogle Scholar
Freyd, P. J. and Kelly, G. M. (1972) Categories of continuous functors I. Journal of Pure and Applied Algebra 2 (3)169–191.CrossRefGoogle Scholar
Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M. and Scott, D. S. (1980) A Compendium of Continuous Lattices, Springer Verlag.CrossRefGoogle Scholar
Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M. and Scott, D. S. (2003) Continuous lattices and domains. In: Encyclopedia of Mathematics and its Applications 93, Cambridge University Press.Google Scholar
Giry, M. (1981) A categorical approach to probability theory. In: Banaschewski, B. (ed.) Categorical Aspects of Topology and Analysis. Springer-Verlag Lecture Notes in Mathematics 915 68–85.CrossRefGoogle Scholar
Goubault-Larrecq, J. (2005) Extensions of valuations. Mathematical Structures in Computer Science 15 (2)271–297. (An early version is available as LSV Research Report LSV-02-17, November 2002.)CrossRefGoogle Scholar
Goubault-Larrecq, J. and Goubault, E. (2003) On the geometry of intuitionistic S4 proofs. Homology, Homotopy and Applications 5 (2)137–209.CrossRefGoogle Scholar
Goubault-Larrecq, J., Lasota, S. and Nowak, D. (2002) Logical relations for monadic types. In: Proceedings of the 16th International Workshop on Computer Science Logic (CSL'02). Springer-Verlag Lecture Notes in Computer Science 2471.CrossRefGoogle Scholar
Goubault-Larrecq, J., Lasota, S. and Nowak, D. (2005) Logical relations for monadic types. Research Report cs.LO/0511006, arXiv.Google Scholar
Heckmann, R. (1990) Power Domain Constructions (Potenzbereich-Konstruktionen), Ph.D. thesis, Universität des Saarlandes.Google Scholar
Hermida, C. A. (1993) Fibrations, logical predicates and indeterminates, Ph.D. thesis, University of Edinburgh, Department of Computer Science. (Also published as ECS-LFCS-93-277.)CrossRefGoogle Scholar
Honsell, F. and Sannella, D. (2002) Prelogical relations. Information and Computation 178 23–43.CrossRefGoogle Scholar
Johnstone, P. (1975) Adjoint lifting theorems for categories of algebras. Bulletin of the London Mathematical Society 7 294–297.CrossRefGoogle Scholar
Jones, C. (1990) Probabilistic Non-Determinism, Ph.D. thesis, University of Edinburgh. (Technical Report ECS-LFCS-90-105.)Google Scholar
Jung, A. (1990) The classification of continuous domains. In: Proc. IEEE Symp. Logic in Computer Science (LICS'90), IEEE Computer Society Press 35–40.Google Scholar
Jung, A. and Tiuryn, J. (1993) A new characterization of lambda definability. In: Proceedings of the 1st International Conference on Typed Lambda-Calculi and Applications (TLCA'93). Springer-Verlag Lecture Notes in Computer Science 664 245–257.CrossRefGoogle Scholar
Kinoshita, Y. and Power, J. (1999) Data-refinement for call-by-value programming languages. In: Proceedings Computer Science Logic, 13th International Workshop, CSL '99, 8th Annual Conference of the EACSL 562–576.CrossRefGoogle Scholar
Larsen, K. G. and Skou, A. (1991) Bisimulation through probabilistic testing. Information and Computation 94 1–28.CrossRefGoogle Scholar
Lazić, R. and Nowak, D. (2000) A unifying approach to data-independence. In: Proceedings of the 11th Internal Conference on Concurrency Theory (CONCUR'2000). Springer-Verlag Lecture Notes in Computer Science 1877 581–595.CrossRefGoogle Scholar
Ma, Q. and Reynolds, J. C. (1992) Types, abstraction, and parametric polymorphism, part 2. In: 7th International Conference on Mathematical Foundations of Programming Semantics (MFPS'91). Springer-Verlag Lecture Notes in Computer Science 598 1–40.CrossRefGoogle Scholar
Mac Lane, S. (1971) Categories for the Working Mathematician, Graduate Texts in Mathematics 5,Springer-Verlag.CrossRefGoogle Scholar
Mitchell, J. C. (1996) Foundations for Programming Languages, MIT Press.Google Scholar
Mitchell, J. C. and Scedrov, A. (1993) Notes on sconing and relators. In: Börger, E., Jäger, G., Kleine Büning, H., Martini, S. and Richter, M. M. (eds.) Proceedings of the 6th International Workshop on Computer Science Logic (CSL'92). Springer-Verlag Lecture Notes in Computer Science 702 352–378.CrossRefGoogle Scholar
Moggi, E. (1991) Notions of computation and monads. Information and Computation 93 55–92.CrossRefGoogle Scholar
Moggi, E. (1995) A semantics for evaluation logic. Fundam. Inform 22 (1/2)117–152.CrossRefGoogle Scholar
Pitts, A. and Stark, I. (1993) Observable properties of higher order functions that dynamically create local names, or: What's new? In: Borzyszkowski, A. and Sokołowski, S. (eds.) Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science (MFCS'93). Springer-Verlag Lecture Notes in Computer Science 711 122–141CrossRefGoogle Scholar
Pitts, A. M. (1991) Evaluation logic. In: Birtwistle, G. (ed.) IVth Higher Order Workshop, Banff 1990, Workshops in Computing, Springer-Verlag 162–189.CrossRefGoogle Scholar
Pitts, A. M. (1996) Relational properties of domains. Information and Computation 127 (2)66–90.CrossRefGoogle Scholar
Plotkin, G., Power, J., Sannella, D. and Tennent, R. (2000) Lax logical relations. In: Proceedings of the 7th International Colloquium on Automata, Languages and Programming (ICALP'2000). Springer-Verlag Lecture Notes in Computer Science 1853 85–102.CrossRefGoogle Scholar
Plotkin, G. D. (1980) Lambda-definability in the full type hierarchy. In: Seldin, J. and Hindley, J. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press 363–373.Google Scholar
Power, J. and Tanaka, M. (2000) Axiomatics for data refinement in call by value programming languages.Google Scholar
Power, J. and Watanabe, H. (2002) Combining a monad and a comonad. Theoretical Computer Science 280 (1-2)137–162.CrossRefGoogle Scholar
Ramsey, N. and Pfeffer, A. (2002) Stochastic lambda calculus and monads of probability distributions. In: Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'02) 154–165.CrossRefGoogle Scholar
Reynolds, J. C. (1983) Types, abstraction and parametric polymorphism. In: Proceedings of the 9th World Computer Congress (IFIP'83), North-Holland513–523.Google Scholar
Rutten, J. (1998) Relators and metric bisimulations. In: Proceedings of the 1th Workshop on Coalgebraic Methods in Computer Science (CMCS '98). Electronic Notes in Theoretical Computer Science 11 1–7.CrossRefGoogle Scholar
Stark, I. (1996) Categorical models for local names. Lisp and Symbolic Computation 9 (1)77–107.CrossRefGoogle Scholar
Stark, I. (1998) Names, equations, relations: Practical ways to reason about new. Fundamenta Informaticae 33 (4)369–396.CrossRefGoogle Scholar
Statman, R. (1985) Logical relations and the typed λ-calculus. Information and Control 65 (2-3)85–97.CrossRefGoogle Scholar
Turi, D. (1996) Functorial Operational Semantics and its Denotational Dual, Ph.D. thesis, Free University, Amsterdam.Google Scholar
Wadler, P. (1992) Comprehending monads. Mathematical Structures in Computer Science 2 461–493.CrossRefGoogle Scholar
Zhang, Y. (2005) Relations logiques cryptographiques – Qu'est-ce que l'équivalence contextuelle des protocoles cryptographiques et comment la prouver? Ph.D. thesis, Laboratoire Spécification et Vérification, Ecole Normale Supérieure de Cachan.Google Scholar
Zhang, Y. and Nowak, D. (2003) Logical relation for dynamic name creation. In: Proceedings of the 17th International Workshop on Computer Science Logic (CSL'03). Springer-Verlag Lecture Notes in Computer Science 2803 575–588.CrossRefGoogle Scholar