On subexponentials, synthetic connectives, and Multi-level delimited control

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

We construct a partially-ordered hierarchy of delimited control operators similar to those of the CPS hierarchy of Danvy and Filinski [5]. However, instead of relying on nested CPS translations, these operators are directly interpreted in linear logic extended with sub exponentials (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.

Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings
EditorsAndrei Voronkov, Ansgar Fehnker, Martin Davis, Annabelle McIver
PublisherSpringer Verlag
Pages297-312
Number of pages16
ISBN (Print)9783662488980
DOIs
Publication statusPublished - 1 Jan 2015
Event20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015 - Suva, Fiji
Duration: 24 Nov 201528 Nov 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9450
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015
Country/TerritoryFiji
CitySuva
Period24/11/1528/11/15

Fingerprint

Dive into the research topics of 'On subexponentials, synthetic connectives, and Multi-level delimited control'. Together they form a unique fingerprint.

Cite this