Sunday, January 5, 2020

All things Rust

Well, this was the best news a while ago (in 2016), thanks Alan Jeffrey!

The slide above was taken from Alan's invited talk at LOLA 2016, Rust for Semanticists (slides in

But I don't think I have made a big song and dance about it in this blog. If I did, I cannot find it now. And I wanted to show it to a young friend, who was asking about PhDs in theoretical computer science. yeah, I had misunderstood his question: he isn't interested in Programming Languages research (shame!) but in Algorithms. oh well, can't win them all.

Now it's sad to notice that most of the work that I did just after my PhD was never published in official venues, i.e proper journals. This was because I was too busy thinking of new stuff, getting married, having kids, trying to find jobs. Some of it was lack of strategic thinking too. So it's particularly nice when someone else recognizes it and calls it out. Now I wonder what else people have been doing with the semantics of Rust, need to check up.

Friday, January 3, 2020

Pleasant Surprise in December

I was looking for ways of doing NER (Named Entity Recognition) in Portuguese and discovered that the spaCy guys have developed an open-source NER system for Portuguese  using our work on Universal Dependencies for Portuguese (paper in

This was a great surprise! I love it!!!

I worry as I don't think the corpus Bosque is good enough. It is small and somewhat old and full of mistakes, but still, the numbers for NER are very good:

NER F 89.18
NER Precision 89.32
NER Recall 89.03

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!