[Prev][Next][Index][Thread]
call-by-value with sums and products
I'm trying to understand the state-of-the-art in call-by-value with
products and sums. Where in the literature would I find, say, Moggi's
computational lambda calculus augmented with sums and products?
(NB: This is distinct from Moggi's monadic metalanguage -- there are
no monads in this calculus, though it is designed to be sound and
complete with regard to translation into the monadic metalanguage.)
The closest I know of is Selinger (2001), who gives an extension of
Moggi's computational lambda calculus with sums and products (as well
as incorporating Parigot's lambda-mu, so it also has, in effect,
call/cc). But Selinger uses equations, not reductions. Where in the
literature would I find equivalent or related systems that use
reductions? Also, his system has the slightly surprising property
that fst(x) and snd(x) are considered as values, where x is a
variable. Are there alternative formulations that avoid this
surprise?
I'll summarize and post the answers. Many thanks! -- P
Peter Selinger, Control Categories and Duality: on the Categorical
Semantics of the Lambda-Mu Calculus Mathematical Structures in
Computer Science 11:207-260, 2001.