Edwardian Proofs in Salvador

In Salvador I talk to Samuel (or perhaps more precisely he talks to me) about lots of things: set theory, the axiom of choice, topological spaces, topological systems and weakenings, nearly countable cardinals and how to show inequalities between them, dialectica categories of different shapes...

This time I gave a Dept Seminar on the Curry-Howard Correspondence and why I think more than simply computer scientists, mathematicians also should be interested in Edwardian proofs and Curry-Howard.

The slides are here, as the talk was a repeat from the one in Boulder, but I will confess that I am not happy with this talk, yet. Alas, I don't know how to make it better, yet.

A Modest Proposal for Portuguese NLP (Four Years Later...)

Four years ago, in September 2010 I gave a three lectures course at EMAp, FGV, Rio de Janeiro, on what I thought one needed to do for a quick ramp up of Portuguese NLP. I had read (diagonally, of course) about many initiatives, I  tried to summarize trends and competencies. And I described the work I had done in the previous nine years at Xerox PARC on a similar project, for English and what it would take to reproduce it in Portuguese, with access to the English code base.


The slides were very preliminary, here are the first ones.

I had a great time, imagining what we could do, if we had lots of people and lots of money. It is always a good thing to give yourself free rein to imagine good outcomes. I should do more of it. Of course nothing good came out of it, in the appropriate timeframe, so I put the proposals in the backburner and got very cross with the verdict that the project was not realistic, that it was too ambitious...

Well, four years later, with no money and only the people that I managed to convince to work for fun, quite a few of the milestones envisaged are in place. This makes me proud.

The slides of a presentation at FGV after four years are here. I also tried to give a more comprehensive picture in a talk in the Dept of Informatica of PUC-Rio, slides here. This work is great fun and there are plenty of things to do, so I hope to get another post going soon with some of the further developments I would like to see.

Textual Entailment Proving LSFA 2014

The "ipe amarelo" was really in bloom in Brasilia for LSFA 2014. Had a great time with friends, old and recent ones.

Talk was too long, my bad. Slides here and the preliminary version of the paper is here.

I also gave a more leisurely presentation of this at COPPE in Rio. The slides are here. It was lovely to see old friends in the audience and to discuss with them this side of my work.


Now I wonder if we can do something much better for the ENTCS proceedings, but the deadline is quite soon and after this time in Brazil, I'm very tired and in need of a rest...

Women in Computing...

I am not big in outreach. I do care passionately for some causes (women in STEM, especially in logic is one of them) and I would love to be able to do more. But with lots of research going on, in different areas, and my pathological inability to organize myself, I find it hard and end up doing very little. Mostly only when people invite me, like for the conference Infinite Possibilities, which was really great.

So I was chuffed to be invited to be part of a roundtable on Women in Computing. Renata Wasserman invited me to the roundtable about Women in Computing that she organized as part of the celebration of 40 years of the Bacharelado em Ciencia da Computacao da USP.

I had some slides from Orna Kupferman that I knew I wanted to use, as  her "scissors diagram" is a powerful communication device. Then I asked my friends about stats from Brazil. Celina Figueiredo, Heloisa and Claudia Bauzer Medeiros, as well as Simone Martins, all had good slides and information. My own version was not as good as I wanted it to be, as I put it together in a great hurry. But altogether it was great fun meeting the "girls" and talking there. Here is a picture in the Happy Hour after the roundtable.

Digital Humanities? Sure, why not?

So we finally have a first paper written, submitted and accepted about work on the DHBB -- the Brazilian Dictionary of Historical Biographies.

This is going to be presented in Guaruja', pretty soon, in the Workshop on Digital Humanities. This was really fun work to do, analyzing the results of text processing with FreeLing
and thinking of ways of improving the information extraction that we could do. I prefer my original title for the work, but reviewers didn't like it, so it's now

Exploratory Information Extraction from a Historical Dictionary

As is to be expected named entities and their recognition play a main role in this project, as do time expressions recognition and multiword expressions. All interesting stuff.

Maude and Isabelle...

Together with Vivek Nigam I am working on proving textual entailment using the traditional rewriting system Maude.

This is an attempt to redo, with open source software, some of the work done in PARC using the Bridge system. What interests me most is the logic we (the PARC Natural Language Theory and Technology team) devised for this task, because the representations in this logic took several years for linguists to agree on. So Vivek and I are taking the short cut of 'assuming' a perfect NLP system. (even explaining what a perfect NLP system means is already kind of long and full of design choices.)

We have a short note, explaining the project, that is to appear in LFSA 2014 in Brasilia. The note builds up from papers describing TIL (Textual Inference Logic) such as A Basic Logic for Textual Inference, Textual Inference Logic: Take Two and Contexts for Quantification.
The note is called  Towards a Rewriting Framework for Textual Entailment.

What about Isabelle? Well, I've been trying to ask people if we could do a parallel implementation in Isabelle and I hope I have convinced Sara Kalvala to do it with me, yepiie!

( I am a member of the group a researchers at the Center for the Study of Language and Information (CSLI) the  Language and Natural Reasoning group, the picture is one of the workshops organized by the group, CSLI Workshop on Natural Logic, Proof Theory, and Computational Semantics, 2011)

BACAT? yes!

My friend Vlad Patryshev organizes the Bay Area Categories And Types  meetup.  

This is a splendid idea, I think. It means people who like the idea of Category Theory and Type Theory can meet and discuss issues, without the pressure of publication and/or competition for spots. I'd love to go more often. I have so far given two talks at BACAT, as we call it.

The first was about partial compilers and dialectica spaces, work of  Mihai Budiu, Joel Galenson and Gordon Plotkin, available from Gordon's webpage.  My slides are here Partial Compilers and Dialectica Spaces. (at the talk I discovered that Mihai is actually the husband of an old friend from PARC days...)

The second talk was on even older work with Gavin Bierman, Nick Benton and Martin Hyland, that we never published properly, only in conferences like TLCA and CSL. This is on deriving a term calculus or a type theory for Intuitionistic Linear Logic, together with its categorical models. I find that the best version is still the technical report (Term Assignment for Intuitionistic Linear Logic) from Cambridge. My recent and over-simplified slides are here Linear Type Theory Revisited.