Our work?

This is an aspirational post. In the Category Theory zulip it has been proposed that people should explain what kind of work they're doing, to help others join them and/or so that young ones can learn who to ask questions, which stuff to read, how to do research, etc. In sum, to make the categories zulip a more cohesive and inclusive community, it might be nice to have more of "our work" posts.

I agree with the reasons heartily. But I have found writing about the work I am doing and want to do kind of difficult. So this is an attempt at disentangling it. 

But the big picture is not helping. Wildfires in California, floods in Louisiana and NYC, drought in the West, melting of glaciers, fires in the whole of South America, the genocide and his accomplices in Brazil, wars and famine getting worse, and of course the plague (picture from the New York Times):

The fact that the wealthiest nation on Earth, where the vaccine is free, is the place with more cases per day of covid19, except for Mongolia, is not lost on people paying attention. It does give me a bad feeling that we're all musicians tuning our instruments to play in the last night before the Titanic sank. Instead of tuning instruments, we should be looking for the lifeboats, the life jackets, the survival tools. But our job is to play music, to do it we need to tune instruments, so that's what we're doing instead. Not a great motivator for our kind of music, really.

Meanwhile, I work in many areas of computing and while I think  the whole research project has unity, this unity is not very clear to the naked eye.  Google Scholar and Semantic Scholar, for instance, tend to think that I am more than one person.  Hence this attempt at discussing the issues.

My work in the Topos Institute is both in applications of Dialectica categories and on Networked Mathematics, together with Brendan Fong. The latter has been discussed in the blog post Introducing the Mathfoldr Project. Work on the dialectica categories has several, interrelated fronts: this is reasonable, as the project has been going on for a very long while. Three papers have appeared recently on the arxiv on dialectica constructions. 

* Davide Trotta spoke about the Godel Fibration (arXiv) recently in the 46th International Symposium on Mathematical Foundations of Computer Science, August 23-27, 2021, Tallinn (Estonia). The blog post about the work with Davide and Matteo Spadetto is here. 

* Elena di Lavore presented a very short poster on the work we did with Wilmer Leal on Dialectica Petri Nets (arXiv). The poster appeared in the Applied Category Theory conference. The blog post is here. 

* I talked about Kolmogorov Problems in the Logic Colloquium in Poland, 2021.  This paper has appeared in a book celebrating the work of my friend and teacher, Professor Paulo Augusto Veloso. The blog post is here.

There is also a blog post on the work with Luiz Carlos Pereira and Elaine Pimentel on Ecumenical systems. This paper we're still writing.

So far, so good. This is the work based on category theory and logic. But not all the work on logic, because Constructive Modal logics made some appearances on two talks  (the one at the Ticamore meeting in June and the one in Celebrating Women in Mathematics  for the group Women in Dynamic Systems in Brazil in May). If they invite me again, I think I can give a much nicer talk now.

A theme I  talked a lot about was the project on Explicit Substitutions for Linear Abstract Machines (xSLAM) with Eike Ritter (University of Birmingham, 1997-2000). I gave three talks about it, because I wanted to make sure that two of the project's main ideas were discussed. The first idea is that type theories for explicit substitutions calculi should have categorical models. This was the one that I discussed intensely. I talked about it in Brasília, Cambridge and at the Topos Institute colloquium.

 The other idea is that indexed categorical models are more powerful than usual 1-categorical models and hence they're able to model a system, called ILT, where we have two implications (intuitionistic and linear) but we do not have a !-modality. This will be discussed next.

One area of my research has been very neglected this year. The work on language did not feature much, unlike the year before. There were many reasons for that, the main one being that Katerina Kalouli finished writing  and defending  her PhD thesis. This is wonderful news! The thesis is really a great piece of work. The inference systems she implemented are a wonderful basis for more experimentation. I am very much looking forward to working on these, as soon as the projects of Topos are clearly engaged. 

Also this year I started working with the Brazilian women doing NLP (thanks Helena Caselli) and this has been lots of fun! I haven't been able to distract Livy Real as much as I wanted to from her real work, but there is always the next weeks!

This post is already too long and I haven't even started on the future work, yet. Of course all the work described is still under development and much more new work should come from it. But other projects are underway too: on mechanizing linear logic (with Elaine Pimentel, Carlos Olarte and Giselle Reis), on 'learning' linear proofs (with Paul Tarau), on our Portuguese wordnet (OpenWordNet-PT) and on Universal Dependencies for Portuguese with Alexandre Rademaker.