TY - JOUR
T1 - Modelling Environments in Call-by-value Programming Languages
AU - Levy, Paul
AU - Power, AJ
AU - Thielecke, Hayo
PY - 2003/9/15
Y1 - 2003/9/15
N2 - 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. (C) 2003 Elsevier Science (USA). All rights reserved.
AB - 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. (C) 2003 Elsevier Science (USA). All rights reserved.
UR - http://www.scopus.com/inward/record.url?scp=0043196810&partnerID=8YFLogxK
U2 - 10.1016/S0890-5401(03)00088-9
DO - 10.1016/S0890-5401(03)00088-9
M3 - Article
VL - 185
SP - 182
EP - 210
JO - Information and Computation
JF - Information and Computation
ER -