Modelling environments in call-by-value programming languages. (English) Zbl 1069.68073
Summary: In categorical semantics, there have traditionally been two approaches to modelling environments, one by use of finite products in cartesian closed categories, the other by use of the base categories of indexed categories with structure. Each requires modifications in order to account for environments in call-by-value programming languages. There have been two more general definitions along both of these lines: the first generalising from cartesian to symmetric premonoidal categories, the second generalising from indexed categories with specified structure to \(\kappa\)-categories. In this paper, we investigate environments in call-by-value languages by analysing a fine-grain variant of Moggi’s computational \(\lambda\)-calculus, giving two equivalent sound and complete classes of models: one given by closed Freyd categories, which are based on symmetric premonoidal categories, the other given by closed \(\kappa\)-categories.
MSC:
| 68Q55 | Semantics in the theory of computing |
| 03B40 | Combinatory logic and lambda calculus |
| 18C50 | Categorical semantics of formal languages |
| 68N15 | Theory of programming languages |
References:
| [1] | Blackwell, R.; Kelly, G. M.; Power, A. J., Two-dimensional monad theory, Journal of Pure and Applied Algebra, 59, 1-41 (1989) · Zbl 0675.18006 |
| [2] | Blute, R.; Cockett, J. R.B.; Seely, R. A.G., Categories for computation in context and unified logic, Journal of Pure and Applied Algebra, 116, 49-98 (1997) · Zbl 0879.03021 |
| [3] | Hasegawa, M., Decomposing typed lambda calculus into a couple of categorical programming languages, (Pitt, D.; Rydeheard, D. E.; Johnstone, P. T., Proceedings of the 6th International Conference on Category Theory and Computer Science (CTCS’95). Proceedings of the 6th International Conference on Category Theory and Computer Science (CTCS’95), LNCS, vol. 953 (1995), Springer: Springer Berlin), 200-219 · Zbl 1502.68055 |
| [4] | B. Jacobs, Categorical Type Theory. PhD thesis, University of Nijmegen, 1991; B. Jacobs, Categorical Type Theory. PhD thesis, University of Nijmegen, 1991 |
| [5] | Kelly, G. M., The Basic Concepts of Enriched Categories (1982), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0709.18501 |
| [6] | Kelly, G. M.; Power, A. J., Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads, Journal of Pure and Applied Algebra, 89, 163-179 (1993) · Zbl 0779.18003 |
| [7] | Levy, P. B., Call-by-push-value: a subsuming paradigm (extended abstract), (Girard, J.-Y, Typed Lambda-Calculi and Applications. Typed Lambda-Calculi and Applications, LNCS, vol. 1581 (1999), Springer: Springer L’Aquila), 228-242 |
| [8] | P.B. Levy, Call-by-push-value, PhD thesis, Queen Mary, University of London, 2001; P.B. Levy, Call-by-push-value, PhD thesis, Queen Mary, University of London, 2001 |
| [9] | Moggi, E., (Computational Lambda Calculus and Monads. Computational Lambda Calculus and Monads, Proc. LICS, 89 (1989), IEEE Press), 14-23 · Zbl 0716.03007 |
| [10] | Moggi, E., Notions of computation and monads, Information and Computation, 93, 55-92 (1991) · Zbl 0723.68073 |
| [11] | Power, A. J., Premonoidal categories as categories with algebraic structure, Theoretical Computer Science, 278, 1-2, 303-321 (2002) · Zbl 1002.68089 |
| [12] | Power, A. J.; Robinson, E. P., Premonoidal categories and notions of computation, Mathematical Structures in Computer Science, 7, 5, 453-468 (1997) · Zbl 0897.18002 |
| [13] | Power, A. J.; Thielecke, H., Environments, continuation semantics and indexed categories, (Proceedings TACS’97. Proceedings TACS’97, LNCS, vol. 1281 (1997), Springer: Springer Berlin), 391-414 · Zbl 0882.18007 |
| [14] | Power, A. J.; Thielecke, H., Closed Freyd- and kappa-categories, (Proceedings ICALP ’99. Proceedings ICALP ’99, LNCS, vol. 1644 (1999), Springer: Springer Berlin), 625-634 · Zbl 0938.03026 |
| [15] | Robinson, E. P., Variations on algebra: monadicity and generalisations of equational theories, Formal Aspects of Computing, 13, 3-5, 308-326 (2002) · Zbl 1004.18005 |
| [16] | Robinson, E. P.; Rosolini, G., Categories of partial maps, Information and Computation, 79, 95-130 (1988) · Zbl 0656.18001 |
| [17] | H. Thielecke, Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, 1997. Also available as technical report ECS-LFCS-97-376; H. Thielecke, Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, 1997. Also available as technical report ECS-LFCS-97-376 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
