Understanding untyped $\overline{\lambda}\mu\widetilde{\mu}$ calculus

Pierre Lescanne (1) , Silvia Likavec (1)

1 LIP - Laboratoire de l'Informatique du Parallélisme

We prove the confluence of $\overline{\lambda}\mu\widetilde{\mu}_T$ and $\overline{\lambda}\mu\widetilde{\mu}_Q$, two well-behaved subcalculi of the $\overline{\lambda}\mu\widetilde{\mu}$ calculus, closed under call-by-value and call-by-name reduction, respectively. Moreover, we give the interpretation of $\overline{\lambda}\mu\widetilde{\mu}_T$ in the category of negated domains, and the interpretation of $\overline{\lambda}\mu\widetilde{\mu}_Q$ in the Kleisli category. To the best of our knowledge this is the first interpretation of $\overline{\lambda}\mu\widetilde{\mu}$ calculus,

On prouve la confluence de $\overline{\lambda}\mu\widetilde{\mu}_T$ and $\overline{\lambda}\mu\widetilde{\mu}_Q$, deux sous-calculs de$\overline{\lambda}\mu\widetilde{\mu}$ dotés de bonnes propriétés et clos par ré duction en appel par nom et en appel par valeur,respectivement. De plus, on donne l’interprétation de $\overline{\lambda}\mu\widetilde{\mu}_T$ dans la catégorie des “domaines niés” et l’interpré tation de$\overline{\lambda}\mu\widetilde{\mu}_Q$ dans la catégorie de Kleisli. Anotre connaissance, cela constitue la premiière non typée du $\overline{\lambda}\mu\widetilde{\mu}$ calcul.

Mots clés: Classical logic; Continuation semantics; Type theory

Mots clés: Sémantique par continuation; Logique classique; Catégories; Théorie des types

Domaines: Informatique [cs]

Pierre Lescanne, Silvia Likavec. Understanding untyped $\overline{\lambda}\mu\widetilde{\mu}$ calculus. [Research Report] LIP RR-2004-50, Laboratoire de l'informatique du parallélisme. 2004, 2+15p. ⟨hal-02101786⟩