On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control
Résumé
We construct a partially-ordered hierarchy of delimited control operators similar to those of the CPS hierarchy of Danvy and Filinski. However, instead of relying on nested CPS translations, these operators are directly interpreted in linear logic extended with subexponentials (i.e., multiple pairs of ! and ?). We construct an independent proof theory for a fragment of this logic based on the principle of focusing. It is then shown that the new constraints placed on the permutation of cuts correspond to multiple levels of delimited control.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...