Lean Logic and Entailment and Contradiction Detection (ECD).
I worked for many years at the Xerox PARC Bridge project and since I am convinced that we did not get to make it as good as it could be, I am engaged in the process of producing a new version, with different tools. Some of this work has to do with lexical resources and connects to work with Gerard de Melo. Some of it is more theorem proving and connects to work with Vivek Nigam. Some of it is really logic and it may connect to Linear Logic.
Lexical Portuguese Resources and OpenWordNet-PT.
OpenWordNet-PT is a Portuguese wordnet we are building. The team includes Alexandre Rademaker, Gerard de Melo, Livy Real, Claudia Freitas and Fabricio Chalub, amongst others. The code is in GitHub and there is a browsable interface.
Constructive Modal Logics and IMLA.
Constructive Modal Logics are very underdeveloped in comparison to classical modal logics. Through the loose organization of several IMLA (Intuitionistic Modal Logics and Applications) workshops we are putting forward our approach, which is mostly based on the Curry-Howard interpretation. This includes work with Gavin Bierman, Nick Benton, Natasha Alechina, Eike Ritter, Michael Mendler, Neil Ghani, amongst others .
Categorical Structures for (Linear) Logic.
For my thesis I worked on categorical models of Linear Logic, then a promising new logic touted for its applications to computing. My thesis uncovered a connection between linear logic and Goedel's Dialectica interpretation boosting linear logic's reputation and, at the same time, reminding logicians of Godel's ingenious way of proving relative consistency of arithmetic. Since then I have described variants of Linear Logic (FILL(Hyland), DILL(Barber and Plotkin), ILT(Maietti and Ritter), etc) and applied new calculi (linear or not), e.g. FIL(Pereira), CS4(Alechina, Mendler), CK(Bellin, Ritter), IHL(Brauner), to modelling phenomena in Computing and Mathematics.