Lean Logic and Entailment and Contradiction Detection (ECD).
I worked for many years at Xerox's PARC on the Bridge project and I am engaged in the process of producing a new version of Bridge, with different and free tools. Some of this work has to do with lexical resources and connects to work below. Some of it has to do with work with Gerard de Melo on a implicative lexicon. 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, http://wnpt.brlcloud.com/wn/.
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 many variants of Linear Logic: FILL(Hyland, Eades), DILL(Barber and Plotkin), ILT(Maietti and Ritter), etc. I have also 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.