Understanding untyped $\overline{\lambda}\mu\widetilde{\mu}$ calculus
Résumé
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.
Origine | Fichiers produits par l'(les) auteur(s) |
---|
Loading...