Skip to Main content Skip to Navigation
Conference papers

On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control

Chuck Liang 1 Dale Miller 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-01239753
Contributor : Dale Miller <>
Submitted on : Tuesday, December 8, 2015 - 11:00:34 AM
Last modification on : Friday, April 30, 2021 - 10:02:40 AM
Long-term archiving on: : Saturday, April 29, 2017 - 10:10:52 AM

File

subdelimlncs.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Chuck Liang, Dale Miller. On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control. LPAR 20 - International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp.297-312, ⟨10.1007/978-3-662-48899-7_21⟩. ⟨hal-01239753⟩

Share

Metrics

Record views

617

Files downloads

350