Algorithmic specifications in linear logic with subexponentials

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Algorithmic specifications in linear logic with subexponentials

Full text

Pdf (521 KB)

Source

International Conference on Principles and Practice of Declarative Programming archive
Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming table of contents

Coimbra, Portugal

SESSION: Expressive logics table of contents

Pages 129-140

Year of Publication: 2009

ISBN:978-1-60558-568-0

Authors

Vivek Nigam	INRIA Saclay - Ile-de France and LIX/Ecole Polytechnique, Palaiseau, France
Dale Miller	INRIA Saclay - Ile-de France and LIX/Ecole Polytechnique, Palaiseau, France

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 4, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1599410.1599427 What is a DOI?

ABSTRACT

The linear logic exponentials !,? are not canonical: one can add to linear logic other such operators, say !^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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. of Logic and Computation, 2(3):297--347, 1992.
	2	David Baelde and Dale Miller. Least and greatest fixed points in linear logic. In N. Dershowitz and A. Voronkov, eds., Intern. Conference on Logic for Programming and Automated Reasoning (LPAR), LNCS 4790, pp. 92--106, 2007.
	3	Jean-Pierre Banâtre and Daniel Le Métayer. Gamma and the chemical reaction model: ten years after. In Coordination programming: mechanisms, models and semantics, pp. 3--41. World Scientific Publishing, IC Press, 1996.
	4	Iliano Cervesato. Typed MSR: Syntax and examples. In MMMACNS: Intern. Workshop on Methods, Models and Architectures for Network Security, LNCS 2052, pages 159--177. Springer, 2001.
	5	Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In G. Gottlob, A. Leitsch, and D. Mundici, eds., Kurt Gödel Colloquium, LNCS 713, pp. 159--171. Springer, 1993.
	6	Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
	7	H. Ganzinger and D. McAllester. Logical algorithms. In Proc. ICLP 2002, LNCS 2401, pp. 209--223. Springer, 2002.
	8	Harald Ganzinger and David A. McAllester. A new meta-complexity theorem for bottom-up logic programs. In R. Goré, A. Leitsch, and T. Nipkow, eds., Automated Reasoning, First Intern. Joint Conference (IJCAR), LNCS 2083, pp. 514--528. Springer, 2001.
	9	David Gelenter. Generative communication in Linda. ACM Trans. on Prog. Lang. and Systems, 7(1):80--112, 1986.
	10	Jean-Yves Girard. Light linear logic. Information and Computation, 143, 1998.
	11	Radha Jagadeesan, Gopalan Nadathur, and Vijay Saraswat. Testing concurrent systems: An interpretation of intuitionistic logic. In FSTTCS, LNCS 3821, pp. 517--528, Hyderabad, 2005. Springer.
	12	Chuck Liang and Dale Miller. Focusing and polarization in intuitionistic logic. In J. Duparc and T.A. Henzinger, eds., CSL 2007 LNCS 4646, pp. 451--465. Springer, 2007.
	13	Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins. Monadic concurrent linear logic programming. In P. Barahona and A. Felty, eds., Intern. ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pp. 35--46, 2005.
	14	D. McAllester. A logical algorithm for ML type inference. In R. Nieuwenhuis, ed., Rewriting Techniques and Applications, 14th Intern. Conference, RTA-03, LNCS 2706, pp. 436--451, Valencia, Spain, 2003. Springer.
	15	David A. McAllester. On the complexity analysis of static analyses. J. ACM, 49(4):512--537, 2002.
	16	Raymond McDowell and Dale Miller. Cut-elimination for a logic with definitions and induction. Theoretical Computer Science, 232:91--119, 2000.
	17	Dale Miller. Forum: A multiple-conclusion specification logic. Theoretical Computer Science, 165(1):201--232, 1996.
	18	Dale Miller and Vivek Nigam. Incorporating tables into proofs. In J. Duparc and T.A. Henzinger, eds., Computer Science Logic, LNCS 4646, pp. 466--480. Springer, 2007.
	19	Dale Miller and Alexis Saurin. From proofs to focused proofs: a modular proof of focalization in linear logic. In J. Duparc and T.A. Henzinger, eds., Computer Science Logic, LNCS 4646, pp. 405--419. Springer, 2007.
	20	Robert J. Simmons and Frank Pfenning. Linear logical algorithms. In L. Aceto, I. Damgård, L. Goldberg, M. Halldórsson, A. Ingólfsdóttir, and I. Walukiewicz, eds., ICALP: Intern. Colloquium Automata, Languages and Programming, Reykjavik, Iceland, LNCS 5126, pp. 336--347. Springer, July 2008.