Ada Lovelace Day 2018

Almost forgot about Ada Lovelace Day again! The interwebs seem to be forgetting too. With all the bad stuff happening in politics and all the accumulated work, caused by (very nice, all the same!!) being Invited Speaker at the Logic AI Summit in Luxembourg, no wonder.

Anyways, my hero figure this year is Professor Christine Paulin-Mohring, Professor Université Paris-Sud and INRIA Saclay - Île-de-France.

Prof Paulin-Mohring  is one of the people responsible for Coq, the famous French theorem prover and an expert on  automated theorem proving using dependent type theory. I have not, so far, recognized any of my heroes of Functional Programming, so this is about time, really. Happy Ada Lovelace Day, Christine!

Mirantão and Linear Dependencies

Mirantão, or actually the `Pensão Renascer' in Mirantão is very pretty.  Rustic, with delicious food, very nice people and landscapes to remind you of a Minas Gerais that only exists in the old songs of Milton Nascimento and Fernando Brant.

But Jornadas Mirantão is not about Club de Esquina nor about the world of Guimarães Rosa, re-inventing o sertão. Jornadas Mirantão are about logic and proof theory in beautiful places. So I talked about an old work with Torben Bra\"u ner that I would like to go back to. This is about using linear dependencies between formulas to describe precisely (and without the support of terms) the system called Full Intuitionistic Linear Logic. The slides are in slideshare and the technical report in Cut-Elimination for Full Intuitionistic Linear Logic. (with Brauner). Technical Report 395 from Computer Laboratory, University of Cambridge and BRICS, Denmark. May 1996.

Playing Mathematician at ICM2018

I am just back from Niteroi, Brazil, where I was Invited Speaker at Logic Satellite event for the International Congress of Mathematicians 2018 (ICM2018) co-organised by the Sociedade Brasileira de Lógica and  DLMPST/IUHPST. This

Division for Logic, Methodology, and Philosophy of Science and Technology

is an alphabet soup that no one can remember properly. The ICM is the  main meeting of  Mathematics around the world, where the Fields Medal, sometimes called the Nobel of Mathematics, is presented every four years. (a bit like the Olympics, really.) I had meant to go for the whole thing, since I have never been to one of these before and since this is the first time it has happened in the Southern Hemisphere, but ended up only being able to go for the Logic event.

The picture of me  comes from Twitter, courtesy of Benedikt Lowe, the Secretary of  the DLMPST 
and one of the main organizers of the logic satellite event. Thanks Benedikt!
I  talked about Relevant Dialectica Categories, which maybe I should talk about in the Nuance NAIL seminar too.

It was very nice of the people in Brazil (especially Bruno Lopes and Samuel Gomes da Silva) to invite me and pay for my trip! and very nice of my manager Charles Ortiz to authorize my PTO. Thank you!

Invited Talks are Fun. Maybe.

I like talking. About work, about politics, about friendship, chit-chat or deep-issues, all are welcome and part of my repertoire.

But yeah, it's especially nice when people ask you to talk about your work. You don't have to submit something and wait for others to decide whether they like it or not, whether they think it's important or not. It's your invited talk, you can do whatever you want. Or so I say.

I feel very lucky to have been invited to talk about my work in a series of occasions. I have a very non-linear working career, with lots of  chop and changing along the way, which, I hope, makes for interesting talks. But clearly also means I don't have all the accolades of the profession. I am, in some sense, still a junior, still hungry to do more work, still not established enough. sigh..

But I digress: the reason I wanted to write this blog post was to remind myself of the other invited talks I've given, to make sure the message I really think it's important is not getting lost in the middle of my own confused mind. That place is a jungle, everything gets lost in there.

I notice that in the curriculum vitae in my webpage from 2016, I kind of list the following invited talks:

1. Weapons of Math Construction, LICS Logic Mentoring Workshop,  Iceland, 2017.
2. Intuitionistic Modal Logic: a personal view, Stanford Logic Seminar, Stanford, CA, USA, 2016
3. Modal Type Theory, Logical and Semantic Frameworks with Applications (LSFA) 2015, Natal, Brazil.
4. Lean Logic for Lean Times: Varieties of Natural Logic, Conference on Computing Natural Reasoning (CoCoNat), Bloomington, Indiana, US, 2015
5. Lean Logic for Lean times: Entailment and Contradiction (ECD) Revisited, 4th CSLI Workshop on Logic, Rationality & Intelligent Interaction, Stanford, CA, US.
6. Intuitionistic Modal Logic: 15 years later, Berkeley Logic Colloquium, Berkeley, CA, USA, 2015.
7. Edwardian Proofs for Futuristic Programs and Personal Assistants,  Plenary Talk, North American Annual Meeting of the Association for Symbolic Logic, Boulder, CO, USA, 2014.
8. Dialectica categories’ surprising application – mapping cardinal invariants, XV Latin American Symposium on Mathematical Logic (SLALM 2012), Bogotá, Colômbia, 2012
9. Edwardian Proofs for Futuristic Programs, Invited Plenary Talk at Infinite Possibilities Conference, IPC2012, Baltimore, Maryland, 2012.
10. A Bridge not too far, SRI AI Seminar, Menlo Park, CA, 2010. 
11. Fibrational Versions of Dialectica Categories.Talk at Stanford Logic Seminar, 2010
12. CLiCS: Categorical Logic in Computer Science, Talk at  M*A*T*H Colloquium, Sonoma State University, 2009.
13. Adventures in SearchLand, PARC Forum, Palo Alto, CA, 2009
14. Constructive Hybrid Logics and Contexts, Hybrid Logic, Seattle, WA, 2006.
15. Dialectica Categories: a survey Logic Lunch Stanford, 1999.
16. Explicit Linear Substitutions,  WoLLIC Sao Paulo, Brazil,  1998. 

Some are more prestigious than others.
I am very proud of having spoken at Infinity Possibilities and the two ASL meetings (Boulder and Bogota). and also especially of the Berkeley Logic Colloquium, where I wanted to ask autographs of the guys in the audience: William Craig, Dana Scott, Paolo Mancuso, John Steel,...
But the hardest was definitely talking about Dialectica categories to Sol Feferman and Grisha Mints when I first arrived in the Bay Area. I miss them!

Old Technical Reports

Nice to find this page from the Computer Lab in Cambridge with my old technical reports, neatly listed, with dates and sizes. This is very helpful, since I was trying to find the original version of the work on Logical Dependencies in Linear Logic, with Torben Brauner.

My Amazon Author page also looks nice, I think.
The only bad thing is the price of the book for Prawitz.
And the stuff not done, yet.

But my page of publications while at PARC disappeared completely. Even from the Wayback Machine, sniff, sniff.

Just as well that Susie Mulhern, a friend that still works for PARC Communications, I think, was able to produce the picture below. I need to do something about it.

Moon over Mongolia and Lexical Resources?

Yep, one has nothing to do with the other. It's just a very pretty picture. I love the fact that the person who took it decided to tell us it's Mongolia. I want to visit China and maybe Mongolia too. Soon. But this post is about Lexical Resources for Portuguese.

It is an awful lot of work to deal with linguistic data. (ok, it can a bit easier than doing mathematics, as everything you do, gets you more data, so it's worth doing it...unlike maths when sometimes it really does not work. ) But we do it! And at least you can look back and see, not only the huge number of things you still want to do but the fairly large number of works you have already done.

This was the spirit of the note "OWN-PT: Taking Stock", which we submitted to NLCS 2018. Alexandre Rademaker gave the talk and had his own slides, which are already the FLoC site. But I produced mine first, so while we think about what to do next and how here they are.

Oxford and FLoC

I admit it: I bit more than I could chew, when I decided to organize three workshops, on different subjects, as part of FLoC2018 (the Federated Logic Conference) in Oxford this July. Sure, I did not know they would be all scheduled for the same weekend. I assumed they wouldn't, but still everything worked fine, mostly.

The picture above is from the dining hall of Wadham College, right after the Workshop Women in Logic 2018. We had a very good workshop and a spirited discussion, "Priorities for Diversity in Logic for Computer Science". Not absolutely clear how we will implement our ideas, but we're working on it.

Then we had Natural Language in Computer Science NLCS2018.  This is the 5th NLCS that  Larry Moss and myself organized, this time we had Ash Asudeh helping us out and the meeting was great! The program is available from FLoC here. Unfortunately I forgot to take pictures during the talks, a real shame! I thought  I had some pictures of the dinner  after NLCS2018 but I cannot found them now...

 Oxford is of course super photogenic... it is difficult to choose which pictures to post.

Finally,  I also also invited by Maribel Fernández, Thomas Ehrhard and Lorenzo Tortora de Falco to help organize the Linearity/TLLA workshop.

The talks were super interesting, but I could not attend. I had several `spies' there, though.  Harley Eades III and Jiaming Jiang, talked about the "Lambek Calculus with an Exchange Modality". Elaine Pimentel   talked about our joint work with Carlos Olarte and Giselle Reis on "Benchmarking Linear Logic Translation". This to the right is a chapel, that is, apparently a library, "where you can work", someone said...

Many intense and productive discussions were had. It was very nice to see good friends that I had not seen for many years.

But there was a big knot on our collective throat: we missed Mike Gordon a lot. As Sara put it, he brought us together once again.