TY - CHAP
T1 - Canonical models for computational effects
AU - Power, John
PY - 2004
Y1 - 2004
N2 - 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.
AB - 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.
UR - http://dx.doi.org/10.1007/978-3-540-24727-2_31
U2 - 10.1007/978-3-540-24727-2_31
DO - 10.1007/978-3-540-24727-2_31
M3 - Chapter or section
VL - 2987
T3 - Lecture Notes in Comput. Sci.
SP - 438
EP - 452
BT - Foundations of Software Science and Computation Structures 7th International Conference, FOSSACS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 – April 2, 2004. Proce
PB - Springer
CY - Berlin
ER -