Sunday, October 13, 2019

Ada Lovelace Day 2019

Better late than never, as they say. Ulrich reminded me, via Twitter, but this was a busy week. So Ada Lovelace Day is only being celebrated today. The idea, and I celebrated every year since 2011, is to have a blog post to celebrate a  woman badass hero.

Christine Ladd-Franklin, Karen Sparck-Jones, Marta Bunge, Helena RasiowaNyedja Nascimento, Manuela Sobral, Maryam Mirzakhani, Christine Paulin-Mohring, so far.

Today I decided to celebrate a cosmologist and astrophysicist,  Angela Olinto. Actually I hardly know what to call Angela these days, as she's the Dean of Physical Sciences of the University of Chicago and so many other things. As the U Chicago magazine describes "This past July, Angela V. Olintothe Albert A. Michelson Distinguished Service Professor in Astronomy and Astrophysics, the Kavli Institute for Cosmological Physics, the Enrico Fermi Institute, and the College, began her appointment as dean of the Physical Sciences Division.

I should explain that "Olinto is best known for her contributions to the study of quark stars, primordial inflation, cosmic magnetic fields, and the origin of the high-energy cosmic rays and neutrinos arriving on Earth from distant galaxies." 

Angela was always my extremely clever friend who was also extremely beautiful and nice. Definitely badass hero! But it also gives me the chance to post the following photo from a long time ago, when we had just won the election for the students union.

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.

Friday, September 27, 2019

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."

Friday, August 23, 2019

Brazil-France Mathematics Meeting

Samuel Gomes da Silva and Elaine Pimentel (together with Boban Velickovic) organized the Mathematical Logic Special Session of the First Brazil-France Mathematics meeting at IMPA in July. I went and talked about our library of propositional intuitionistic theorems, described in
The ILLTP Library for Intuitionistic Linear Logic
C Olarte, V de Paiva, E Pimentel, G Reis
arXiv preprint arXiv:1904.06850

Lots of interesting conversations in the meeting. All the slides of the meeting were collected  and can be found in this Google drive folder. Other mathematical logic meetings associated with the UFBA are described here.

Thursday, August 15, 2019

Adventures in SearchLand, rediscovered

So I found the video of my PARC Forum in 2009! yay!
It's now in YouTube in my channel (doesn't this sound funny?), at, YouTube informs me.

But this took quite a while, including finding an old computer with DVD reader, finding a charger that's by now two models behind,  downloading rippers and waiting forever for YouTube to decide to accept my video. oh well, it's done now.

The slides have been in SlideShare since 2012, and the real paper is still to be written. of course.

The pictures have nothing to do with the talk. They're just to remind me that we can still be silly and have some fun. Ana is still the best!

Saturday, August 10, 2019

Summer 2019 is over. or almost over.

 I took this picture before the beginning of the Encontro de Mulheres Matematicas, in IMPA, Rio de Janeiro, 27 July 2019. The excitement is palpable, we're all ready to go, all eager to show that Mathematics -- in all its diversity-- is our passion.

I had a wonderful time and made several new friends. I was also in awe of the ability of my new friends, they are so competent, so  able to communicate their mathematics, I felt a tad jealous. I wish I was that competent at their age. This was a great way to close this Summer.

I think it was even worth missing Eric's graduation for it. He promised me that there will be another graduation soon enough. For the time being I only have the photos and the short video that Richard took. The pictures of Cornwall are lovely!

Meanwhile this is a picture of the end of the meeting on Women Mathematicians. It was a huge success, people came from everywhere in Brazil for the meeting.
One girl had to go 24 hours by boat, to get to Manaus and then fly in!! This is dedication beyond the call of duty.

Now I just read the column of Marcelo Viana, director of IMPA after the meeting, "What women want after all" is a rough translation. Amazing the level of lack of understanding of some mathematicians. To be absolutely clear, I don't mean lack of understanding on Viana's part, but of the people he quoted. Goodness me.

Tuesday, July 16, 2019

Skype Talk in May: Round Table at EBL

I couldn't go to the Encontro Brasileiro de Logica (EBL) in Joao Pessoa this year. I wanted to, as I went to the last one in Paraiba, too many years ago, and had a great time.

This time we (Gisele Secco, Elaine Pimentel, Claudia Nalon and myself) had offered to organize a round table about Women in Logic. And so we did, yay! I spoke over Skype, not the best medium, but what can be done, can be done.

We hope to have a text about it written sometime soon. Meanwhile, slides are in slideshare.