Abstract
Given a signature of basic operations for a computational effect such as side-effects, interactive input/output, or exceptions, we give a unified construction that determines equations that should hold between derived operations of the same arity. We then show how to construct a canonical model for the signature, together with the first-order fragment of the computational λ-calculus, subject to the equations, done at the level of generality of an arbitrary computational effect. We prove a universality theorem that characterises the canonical model, and we recall, from a previous paper, how to extend such models to the full computational λ-calculus. Our leading example is that of side-effects, with occasional reference to interactive input/output, exceptions, and nondeterminism.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Benton, N., Hughes, J., Moggi, E.: Monads and effects. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 42–122. Springer, Heidelberg (2002)
Carboni, A., Lack, S., Walters, R.F.C.: Introduction to extensive and distributive categories. J. Pure Appl. Algebra 84, 145–158 (1993)
Fiore, M., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: Proc. LICS 1999, pp. 214–224. IEEE Press, Washington (1999)
Hyland, M., Levy, P.B., Plotkin, G.D., Power, A.J.: Combining continuations with other effects (submitted)
Hyland, M., Plotkin, G.D., Power, A.J.: Combining computational effects: commutativity and sum. In: Proc. IFIP Conf. On Theoretical Computer Science, pp. 474–484. Kluwer, Dordrecht (2002)
Hyland, M., Plotkin, G.D., Power, A.J.: Combining computational effects: sum and tensor (submitted)
Kinoshita, Y., Power, A.J.: Data Refinement in Call-by-Value Languages. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 562–576. Springer, Heidelberg (1999)
Levy, P.B., Power, A.J., Thielecke, H.: Modelling environments in call-by-value programming languages. Information and Computation 185, 182–210 (2003)
Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic. Springer, Berlin (1992)
Moggi, E.: Computational lambda-calculus and monads. In: Proc. LICS 1989, pp. 14–23. IEEE Press, Washington (1989)
Moggi, E.: Notions of computation and monads. Inf. and Comp. 93(1), 55–92 (1991)
Moggi, E.: A Semantics for Evaluation Logic. Fundamenta Informaticae 22 (1995)
Plotkin, G.D., Power, A.J.: Adequacy for Algebraic Effects. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 1–24. Springer, Heidelberg (2001)
Plotkin, G.D., Power, A.J.: Notions of Computation Determine Monads. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 342–356. Springer, Heidelberg (2002)
Plotkin, G.D., Power, A.J.: Algebraic Operations and Generic Effects. In: Proc. MFCSIT 2000, Applied Categorical Structures, vol. 11(1), pp. 69–94 (2003)
Plotkin, G.D., Power, A.J.: Computational Effects and Operations: an Overview. In: Proc. Domains 2002. ENTCS, vol. 73 (2002)
Plotkin, G.D., Power, A.J.: Logic for Computational Effects. In: Proc. International Workshop on Formal Methods 2003 (to appear)
Power, A.J.: Models of the Computational λ-calculus. In: Proc. MFCSIT 2000. ENTCS, vol. 40 (2001)
Power, A.J.: Premonoidal categories as categories with algebraic structure. Theoretical Computer Science 278, 303–321 (2002)
Power, A.J.: A Universal Embedding for the Higher Order Structure of Computational Effects. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 301–315. Springer, Heidelberg (2003)
Power, A. J., Robinson, E.P.: Premonoidal categories and notions of computation. In: Proc. LDPL 1996. Math Structures in Computer Science, vol. 7, pp. 453–468 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Power, J. (2004). Canonical Models for Computational Effects. In: Walukiewicz, I. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2004. Lecture Notes in Computer Science, vol 2987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24727-2_31
Download citation
DOI: https://doi.org/10.1007/978-3-540-24727-2_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21298-0
Online ISBN: 978-3-540-24727-2
eBook Packages: Springer Book Archive