Call-by-value is dual to call-by-name - Reloaded

We consider the relation of the dual calculus of Wadler (2003) to the lambda mu-calculus of Parigot (1992). We give translations from the AIL-calculus into the dual calculus and back again. The translations form an equational correspondence as defined by Sabry and Felleisen (1993). In particular, translating from lambda mu to dual and then 'reloading' from dual back into lambda mu yields a term equal to the original term. Composing the translations with duality on the dual calculus yields an involutive notion of duality on the lambda mu-calculus. A previous notion of duality on the lambda mu-calculus has been suggested by Selinger (2001), but it is not involutive.