Sunday, September 29, 2019

A bibliography of Linear Logic? Again?



A while back there was a bibliography of Linear Logic, started, I believe in Amsterdam for Anne Troelstra's book "Lectures on Linear Logic" (CSLI Lecture Notes No. 29, Center for the Study of Language and Information, 1992) by Harold Schellinx, but then moved to Carnegie Mellon where Iliano Cervesato  and Carsten Schürmann  looked after it, for a while. But the last update was in 1998, apparently. So when someone I didn't know asked in the LOGICA-L mailing list why no one worked in Linear Logic, what was happening in Linear Logic, I didn't know what to reply.

Just as well that Carlos Olarte, my co-author in some recent work on implementing a benchmark of sorts for Linear Logic, was quick to answer. Carlos showed some recent work on Linear Logic, particularly from Brazilians and particularly in the applications that he's interested in.

Here's his list:
[1] Vivek Nigam, Carlos Olarte, Elaine Pimentel: On subexponentials, focusing and modalities in concurrent systems. Theor. Comput. Sci. 693: 35-58 (2017)
[2] Elaine Pimentel, Carlos Olarte, Vivek Nigam: A Proof Theoretic Study of Soft Concurrent Constraint Programming. TPLP 14(4-5): 649-663 (2014)
[3] Vivek Nigam, Dale Miller: A Framework for Proof Systems. J. Autom. Reasoning 45(2): 157-188 (2010)
[4] Dale Miller, Elaine Pimentel: A formal framework for specifying sequent calculus proof systems. Theor. Comput. Sci. 474: 98-116 (2013)
[5] Carlos Olarte, Elaine Pimentel: On concurrent behaviors and focusing in linear logic. Theor. Comput. Sci. 685: 46-64 (2017)
[6] Vivek Nigam, Dale Miller: Algorithmic specifications in linear logic with subexponentials. PPDP 2009: 129-140
[7] Carlos Olarte, Elaine Pimentel, Camilo Rueda: A concurrent constraint programming interpretation of access permissions. TPLP 18(2): 252-295 (2018)
[8] Joëlle Despeyroux, Carlos Olarte, Elaine Pimentel: Hybrid and Subexponential Linear Logics. Electr. Notes Theor. Comput. Sci. 332: 95-111 (2017)
[9] Timo Lang, Carlos Olarte, Elaine Pimentel, Christian G. Fermüller: A Game Model for Proofs with Costs. TABLEAUX 2019: 241-258
[10] Carlos Olarte, Valeria de Paiva, Elaine Pimentel, Giselle Reis: The ILLTP Library for Intuitionistic Linear Logic. Linearity-TLLA@FLoC 2018: 118-132
[11] Kaustuv Chaudhuri, Leonardo Lima, Giselle Reis: Formalized meta-theory of sequent calculi for linear logics. Theor. Comput. Sci. 781: 24-38 (2019)
[12]  Bruno Xavier, Carlos Olarte, Giselle Reis, Vivek Nigam: Mechanizing Focused Linear Logic in Coq. Electr. Notes Theor. Comput. Sci. 338: 219-236 (2018)
[13] Vivek Nigam, Elaine Pimentel, Giselle Reis: Specifying Proof Systems in Linear Logic with Subexponentials. Electr. Notes Theor. Comput. Sci. 269: 109-123 (2011)
[14]  Vivek Nigam, Giselle Reis, Leonardo Lima: Quati: An Automated Tool for Proving Permutation Lemmas. IJCAR 2014: 255-261
[15]  Jean-Yves Girard, Paul Taylor, Yves Lafont, Proofs and Types. Cambridge University Press. 
[16] Anne Sjerp Troelstra, Helmut Schwichtenberg: Basic proof theory, Second Edition. Cambridge tracts in theoretical computer science 43, Cambridge University Press 2000, ISBN 978-0-521-77911-1, pp. I-XII, 1-417
[17] Jean-Yves Girard: Linear Logic. Theor. Comput. Sci. 50: 1-102 (1987).

Lots of interesting papers in this list, for sure. But I was left with a feeling that I should be able to list all the areas of applications (both the ones I like and the ones I am not very fond of) and that a reasonably updated bibliography was missing. So I thought I would start a GitHub repo for that, using Google Scholar and looking through the citations of Girard's original paper "Linear Logic. Theor. Comput. Sci. 50: 1-102 (1987)".

This doesn't even have my own papers in it, yet.
But one has to start somewhere.

The lovely boy in the picture is Alan Turing, in case you didn't recognize him. Courtesy of Charles Ortiz Jr.

No comments:

Post a Comment