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.

Brazilian Women in Mathematics

This is not the picture used in the blog about the Invited Talk, in which I look really bad.
This one is not great, but it's from the same day and I don't think it is too ugly. Besides, it has Jacqueline too, which is definitely a good thing!

Here I am just posting the write-up about the talk, written by the IMPA Communications journalist, Karine Rodrigues, which I liked very much (Thanks, Karine!). Ok, the write-up did make me ten years older than I am, but still, it gets (most of) the mathematics and why I like it, RIGHT and this is the main thing.

(Here's a Google translation of her text, adapted)

With the experience of those who built an enviable trajectory in more than three decades in research, with traffic in the academy and in Silicon Valley, the Brazilian Valeria de Paiva considers that the situation of women in Science, Technology, Engineering and Mathematics (STEM) is still "o fim da picada" (in colloquial Portuguese, "the pits").

Invited to give one of the special lectures of the Brazilian Meeting of Mathematical Women, held this weekend at IMPA, in Rio de Janeiro, the mathematician gave an interview to IMPA and talked about gender issues in science. Citing data from a survey conducted by the American Association of University Women (AAUW), Valeria notes that in the United States, the proportion of women employed in both areas fell between 1990 and 2013: from 35% to 26%. In Engineering, the movement was at least growth, but it was very shy, going from 9% to 12%.
"In the United States, at least, and I believe the statistics here in Brazil are not very different, the situation has worsened, if we consider, for example, Mathematics and Computation," emphasizes the researcher, who also began to devote herself to discussions. of gender in science in the last decade.

In the lecture that opened the programming of the second and last day of the event, “From Pure Algebra to Applied Category Theory: a personal journey”, Valeria spoke briefly about her trajectory between the Bachelor of Mathematics at PUC Rio in the early-1980s, and the current work at Samsung Research America where she helps create new products using Artificial Intelligence.

Before moving to Silicon Valley, she was a researcher at Cambridge University and Birmingham University in the United Kingdom. In Cambridge, having been supervised by Martin Hyland in her "Dialectica Categories" thesis, the researcher has as her academic great-grandfather none other than Alan Turing (1912-1954), considered the father of computing.

A specialist in Category Theory, an area that deals abstractly with mathematical structures and the relationships between them, Valeria explained, for example, how pure mathematics guides computation through the Curry-Howard Correspondence -- in programming language theory.
This is the direct relationship between computer programs and mathematical proofs, mediated by algebra/category theory.

"What I do is to use Category Theory, which is considered one of the purest areas of mathematics, in database computing applications, quantum computing, natural language semantics, and all of those things that seem very different from each other, but are actually deeply related," she joked. According to her, "this correspondence between such structures is a hidden gem of Mathematics, which relates logic to algebra and computing in a very surprising way."