On untyped Curien-Herbelin calculus

We prove the confluence of λμμeT and λμμeQ, two well-behaved subcalculi of Curien and Herbelin’s λμμe calculus, stable under call-by- name and call-by-value reduction, respectively. Moreover, we study the semantics of λμμe calculus, give the interpretation of λμμeT and λμμeQ using the category of negated domains and the Kleisli category. To the best of our knowledge, this is the first interpretation of untyped λμμe calculus. We also give a thorough overview of the work on continuation semantics.