(sigemb-info 333) Talk by Daisuke Kimura at RIMS, Kyoto U, Thu 27 Nov 2008

["Ichiro Hasuo" <ichiro@xxxxxxxxxxxxxxxxxxxx>]

Dear all,

Let me advertise a talk by Daisuke Kimura (NII) at RIMS, Kyoto Univ.
No registration necessary. See you there!

Best regards,
Ichiro Hasuo
http://www.kurims.kyoto-u.ac.jp/~cs/

======

Daisuke Kimura (National Inst. Informatics)
Computational duality and Logical duality
11.00 - 12.00, Thu 27 Nov 2008
CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see
http://www.kurims.kyoto-u.ac.jp/~cs/lab.html for direction )

Abstract:
Computational duality between call-by-value and call-by-name is
closely related to logical duality of classical logic that is known as
de Morgan duality. Selinger gave a categorical semantics of the
lambda-mu-calculus, and explained this relationship by using the
category-theoretic duality. Wadler introduced the dual calculus that
corresponds to classical sequent calcul us, and explained it in a
purely syntactical way. However, their result was based on equational
theories. Wadler left an open question whether one can obtain similar
results by replacing the equations of his work with reductions. This
talk presents the best possible answer to his question.

We first refine the lambda-mu-calculus as reduction systems by
reformulating sum types and omitting problematic reduction rules that
are not simulated by Cut-elimination procedures. Secondly, we give
reduction preserving translatio ns between the call-by-name
lambda-mu-calculus and dual-calculus. We show that the compositions of
these translations become identity maps up to the call-by-name
reductions. We also give translations for the call-by-val ue systems,
and show that they satisfy properties similar to the call-by-name
case. Thirdly, we introduce translations between the call-by-value and
call-by-name lambda-mu-calculi by composing the above translations
with duality on the dual c alculus. We finally obtain results
corresponding to Wadler's, but our results are based o n reductions.