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 Rasiowa,  Nyedja 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. Olinto, the 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.

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

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.

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
https://www.youtube.com/watch?v=yxkHAQitTdg, 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, https://www.slideshare.net/valeria.depaiva/parc-forum-2009-adventures-in-searchland 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!

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.

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.https://www.slideshare.net/valeria.depaiva/mulheres-na-logica-e-no-brasil

BACAT2019: Petri nets rewind

This  only appeared briefly in twitter.

A total contrast between  Santa Clara at 7 pm in February and at 7 pm in June.

A great discussion on Petri nets, using the Dialectica construction.

Slides are in slideshare. Somehow the questions became about pros and cons of dialectica versus Chu construction, I mentioned Dialectica and Chu constructions: cousins,  (Theory and Applications of Categories, vol 17 Issue 7, pages 127-152, 2007) because I have always wanted a "Dialectica Calculator", like the "Chu calculator" Vaughan Pratt has. But I realized that the line "there are pros and cons to both" is not very informative. I need to go back to that.

One of the reasons I still want to write about Petri nets, using the dialectica model is because I hope that morphisms that are simulations, instead of bisimulations or other more strict maps, might be more useful in practice. (Need to find a way of checking on this properly)

But then I got thinking that the mathematics of Chu construction is somewhat easier, as more symmetric, so maybe those Petri nets make sense too?

Vancouver in June

We had Women in Logic 2019 in Vancouver, British Columbia, Canada.
There are some photos in FB's group Women in Logic.
It was a neck-breaking speedy trip, I was in Vancouver for one night only, but well worth it.
The meeting was smaller than the one in Oxford last year, as expected. FLoC does encourage lots of people to come, who wouldn't otherwise.

But the meeting was very productive with decisions taken, committees organized, bold plans for 2020. Also a general feeling that we can do this together and it will be just fine! Very grateful for that. I was worried about (not) missing my plane back home (I almost missed it going out), so didn't have much time to enjoy the brewery, but had plenty of good conversations over sushi at lunchtime.

  Another lesson learned is that for a short workshop is very important to plan the social events in advance.  It worked well for us, we found good restaurants close by, but it should've been announced earlier on. We almost missed Ana Sokolova!

But all's well that ends well, we were all seated for beer eventually.

Tuebingen in March

I had an amazing time in Tuebingen in March. The meeting was fantastic! Thanks Peter Schroeder-Heister and Thomas Piecha for a great programme, excellent accommodations and an amazingly beautiful place. Having  just started at Samsung Research America two weeks earlier, I was a bit worried about flying off, but I had   bargained for the trip,  and all was fine.

Farewell to Prof Troelstra

This year has, so far, being complicated with a somewhat traumatic job move, from Nuance to Samsung Research America. I started in Samsung in  March 2019 and hence have not had the time to grieve properly over the departure of Prof Anne Troelstra in March 2019, after a brief illness. The Institute for Logic, Language and Computation of the University of Amsterdam has an obituary for him and several condolence messages. Personally I knew and admired Prof Troelstra very much. I was invited once by him to Amsterdam to discuss logic and, yes, he could be very intimidating, but once you got over that, he was a very generous mathematician. Someone you could ask questions and trust the answers. Someone who, over a blackboard, would treat you as if you were a colleague, instead of a mere  phd student starting to think about things. Someone willing to entertain very different ideas, at least for the time of the discussion. 
Rest in power, Anne!

Together with Grigori Mints,  Solomon Feferman, Danny Bobrow and Aurelio Carboni, another mentor lost.

 

Mycroft and SNIPS: open source voice assistants

Any excuse to have Sherlock on the blog is good, I say. This time I want to record the fact that there is an open source voice assistant, called Mycroft, code available from GitHub, originating from Kansas City, MO, they say. Mycroft, like Alexa and Bixby, has skills contributed by the community of users. I wanted to buy Mycroft Mark 2, but this seems to be out of stock right now.

The other open source voice assistant is called snips. They have a different storyline in mind and Jarvis is the module that creates a voice assistant for free, in different languages. Then one can deploy the assistant to a Raspberry Pi, an Android or a Linux device. This will run completely on-device, keeping data safe and private! 
The Snips Platform is a software solution powering Private-by-Design voice assistants. Businesses or individuals, anyone can set up the Snips Platform on a single board computer (for example a Raspberry Pi 3, an i.MX8M board, an Android or an iOS device), and install a voice assistant on it.

Alexa has by now apparently 70K skills and I don't know how many `tasks' in Google Home Assistant market place. I wonder if anyone has written a comparison of all these voice frameworks.

Natural Language Inference: over and over again

This post is about collecting the many talks I have given about Natural Language Inference.
The first one is from the beginning of 2017 and has not been written up as a paper, yet. The slides of Universal Dependencies for Inference from Feb 2017 are in SlideShare.

Then the work with Katerina Kalouli and Livy Real, that ended up in several papers, is described in the slide deck Natural Language Inference: logic from humans, from December 2017.

Further,  I talked in Oslo on Natural Language Inference in SICK at the  MAy 2018 workshop on Meaningful Work: Advancing Computational Semantics. There I met Martha Palmer and more collaboration ensued, yay!

Vanity Trip

Nice things in the past? Nah! Building my brand? I wish!

Anyways, this post is about situations where people said nice things about my work.

So, I am very proud of my Wikipediapage,  
https://en.wikipedia.org/wiki/Valeria_de_Paiva. A `friend' suggested that, if I had created my own page, at least I had the grace of not getting caught. With friends like this, who needs enemies, right?

When I was still at Xerox PARC, the MAA did this piece https://www.maa.org/careers/career-profiles/academia-teaching/valeria-de-paiva. After I left PARC, I was invited to come back and give a PARC Forum, something I was never invited to do during the nine years I spent there. I think the talk and the poster (reduced image below) turned out quite well. The video was on the PARC website, at https://www.parc.com/parc-forum/adventures-in-searchland/, but  it's now gone. After all, this was nine years ago. (I think I still have the DVD of the talk, I should try to convert it to digital. update: I did, the talk is now at youtube.)

After  many years, when I was at Nuance, AMS's Math Awareness Month did this interview with me http://www.mathaware.org/mam/2015/highlighted/MAM%202015%20profile_dePaiva.pdf (this seems to have disappeared from the live web, wayback machine to the rescue) and I was delighted.  But the most amazing was to discover, when searching the Web for something else,  this pretty cartoon done by the guys at Karisma.org, from Colombia, within the blog post https://karisma.org.co/que-pasaria-sin-el-aporte-de-las-mujeres-a-la-ciencia-en-el-mundo/.

Sadly the profile that the Samsung comms did about me was only internal and I don't know if I have a copy somewhere. I will add it here if I find it. But recently there was also this  report on this (self-referential) blog which was very cool!

The old poster from MAM (Mathematical Awareness Month) is below, thanks to the Wisconsin Dept of Public Instruction.

 

Old Stories

This amazing picture taken, I presume, at Pico da Neblina, Brazil reminds me very much of Isabel Allende's young adult novel City of the Beasts.  I liked it very much when I first read it. Rechecking it in Wikipedia just now, I guess I  am really not very sophisticated in my love of books.

Anyways, the point of this post is to remember old stories of a very different kind. This deck contains the slides of my first talk at Nuance, in October 2012.

To show, once again, that I really need to be better at organizing my work, I talked about this deck  in this blog post, in this one and in this post.

Old (2017) BACAT slides

I'm pretty useless at keeping track of what I have and have not done and when. So here are the slides from when I talked in BACAT in Sept 2017 about Temporal Logic, "Doing Time, Categorically".

This was a paper with my collaborator Harley Eades III for a special issue of the IfColog Journal in honour of Grigori Mints. I feel that I need to improve on this paper and I also need to carry on with the project of constructive modal logics, but not now, as other requests on my time are taking precedence.

Santa Clara in February

Yesterday I talked at BACAT (Bay Area Categories And Types) and it was a lot of fun. When I searched for my old slides  I thought that I hadn't spoken at BACAT for a long while, since 2014. But this was only because I cannot find anything on my computer. In reality, I had talked in Sept 2017 about temporal logic. Still, this was a long time ago and the old building where Computer Science had classes has been demolished.

But the campus is now looking lovely and I wish I had taken pictures.

The slides for the talk are here.  I liked my title "Going Without: a modality and its role" because the ambiguity works on my favour, for once. The slides are a bit rough, as BACAT talks are fun because you can afford to be tongue-in-cheek and outrageous, if you so wish.

Organizing Talks

Organizing talks is an art, and as such, it can be lots of hard work, as well as plenty of fun. But since it happens bit by bit you can only see how hard you've worked with hindsight. I've organized six years of talks at Nuance Sunnyvale Lab, 202 talks, in total, I believe.

Sure, lots of other people helped too, but I think most of the work was actually mine. There were times that I thought it was a waste of time and thought I'd stop doing it. But I really enjoy listening to engaging talks, and I do have plenty of very engaging friends, so I usually went back to organizing it. Most of the talks were academic and about stuff already published. I do not have the abstracts or slides for most of the talks, so I hope none of the presenters will be offended that in the attachment there is simply a spreadsheet with their name and the titles of the talks.

Google Plus is going away

So Google decided to shut down Google+. A shame as the product always gave me the mistaken impression that I had some sort of internet presence. You see, I do have (and follow) a few famous friends and some of their fame 'splashes' over me. Anyways the reason for this post is to try to remind me to save all the bits of writing and links I have in the service. Because the last two times Google terminated a product I was to busy to save my data and I regret it (bitterly) to this day. I lost an immense number of photos...

Amsterdam in January

I'm flying back to California tomorrow, after a week in Amsterdam. The conference SYSMICS  2019 (http://events.illc.uva.nl/SYSMICS2019/) was great. Plenty of interesting talks on all kinds of stuff that I like: dualities, Heyting algebras, lax logic,  topologies, you name it. Several conversations on Dialectica categories and what I (still) want to do with them

Very grateful to Yde Venema and Nick Bezhanishvili for inviting me!

The conversations outside the official talks were great too. There was an Evening Lecture on AI, given by Frank van Harmelen that was great fun, once I managed to find my way there, without being run over by an angry cyclist. Quite amazing how even with an iphone and various kinds of maps, I can still get lost and walk in the opposite direction from the one I am trying to go.

But the best of non-work stuff was hanging out with Jan van Eijck and Heleen Verleur for her play and music concert and chats. Thanks Jan!