Retour à la page du séminaire

11h : P.L. Curien et H. Herbelin (PPS)
On the duality of call-by-name and call-by-value.

résumé

Nous présentons une syntaxe LK_mu_mu tilde pour le calcul des séquents classique (connecteur implication) qui permet via l'isomorphisme de Curry-Howard d'exhiber des symétries de calcul telles que programme/contexte et appel par nom / appel par valeur. Dans notre syntaxe, choisir la discipline appel par nom / appel par valeur pour la réduction se ramène à choisir l'une des deux orientations symétriques d'une paire critique (qui est une version polarisée de celle de Berardi et Barbanera). Notre analyse nous conduit à revisiter la question de savoir ce qu'est une syntaxe naturelle fonctionnelle pour le calcul par valeur. On définit une traduction du lambda-mu-calcul dans LK_mu_mu tilde et une traduction de LK_mu_mu tilde dans le lambda-calcul, et nous retrouvons des traductions CPS connues en composant ces traductions de manière appropriée.