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

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.