Skip to Main content Skip to Navigation
New interface
Conference papers

Algorithmic specifications in linear logic with subexponentials

Nigam Vivek Dale Miller 1, 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 : The linear logic exponentials !, ? are not canonical: one can add to linear logic other such operators, say !^l, ?^l, which may or may not allow contraction and weakening, and where l is from some pre-ordered set of labels. We shall call these additional operators subexponentials and use them to assign locations to multisets of formulas within a linear logic programming setting. Treating locations as subexponentials greatly increases the algorithmic expressiveness of logic. To illustrate this new expressiveness, we show that focused proof search can be precisely linked to a simple algorithmic specification language that contains while-loops, conditionals, and insertion into and deletion from multisets. We also give some general conditions for when a focused proof step can be executed in constant time. In addition, we propose a new logical connective that allows for the creation of new subexponentials, thereby further augmenting the algorithmic expressiveness of logic.
Document type :
Conference papers
Complete list of metadata
Contributor : Dale Miller Connect in order to contact the contributor
Submitted on : Thursday, January 10, 2013 - 1:21:41 PM
Last modification on : Thursday, January 20, 2022 - 5:30:47 PM


  • HAL Id : hal-00772332, version 1



Nigam Vivek, Dale Miller. Algorithmic specifications in linear logic with subexponentials. PPDP09 - ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Sep 2009, Coimbra, Portugal. ⟨hal-00772332⟩



Record views