Thursday, November 29, 2012

Dick Tracy

Since I am fed up with having to google these two whenever I need to explain to someone why my plans are possible, albeit non-trivial, here they are:

Dick-Tracy paper on Unified Lexicon and on Transfer "semantics".

Oops forgot another important one, Crouch on KR and semantics,  2005.

Wednesday, November 21, 2012

Being thankful...

Araquem Alcantara is an amazing photographer. I want to buy all his books...but despite the beautiful picture of the Mata Atlantica, this post is only about good stuff that happened to me this week as far as work is concerned.

So the paper with Patricia, Cleo and Annie ("Where's the meeting that was cancelled?") was accepted for the COLING workshop on Cognitive Aspects of the Lexicon. The reviewers don't seem to agree with me that inferential aspects are the main cognitive issue that the lexicon needs to address, but they found the work intriguing enough to accept it for the workshop. Good. There are lots of inferential aspects to the lexicon, we only touched some in the paper, which continues the work on Computing Relative Polarity for Textual Inference,  Context Inducing Nouns and Simple and Phrasal Implicatives. (I don't know if Lauri or Annie have written about the work on inferential aspects of adjectives/adverbs, but I guess they must have too.) Anyway this project is big and there is lots still to do and it would be good to get the lexicographers excited about it.

But there are lots of mundane issues for the workshop, visas, passports, and most of all time. Do I have time to go to Mumbai, India? I love the idea. I thought I did have the time, but  now  that I discovered that I need a new passport for the trip,  a decision  has been taken and I'm not going. sniff...

The paper with Marcela, Ju and Ruy on intuitionistc n-graphs was also accepted for the special issue of the Journal of the IGPL devoted to the Brazilian Logic colloquium EBL. This is good too. But again there are lots to do, as this is the simple first step...

Different first steps in different blog posts, Valeria!

Wednesday, November 7, 2012

Jabuticaba? always...

Being too busy with the new job to write anything here.

Also elections both here (the zombie apocalipse -- sorry if you feel offended zombies!-- has been averted) and in Brazil (don't know really what to say...) meant much to read, no time to write.

But must remember: early November, later October is jabuticaba (or jaboticaba) time in Brazil.  Next year must organize to be there at the right time! and ask for repeat invitation from  my cousin Alvaro Vaz, who took the beautiful picture...

Shouldn't be too hard. Anonymous was everywhere last Monday with Guy Fawkes little rhyme "Remember, remember the 5th of November..."

Oh well, this is an odd cultural melange, if I've ever seen one: Guy Fawkes, anti-catholicism, anonymous, V for Vendetta,  Sandy, Diwali, elections and jabuticaba...ftw? certainly the jabuticaba.

Saturday, October 27, 2012

Flu shot causes cold?

It doesn't make sense, but it's the second time that it happens to me.
So sitting in the couch, feeling really poorly. and downloading software, so I can do some proper work next week.

But I don't know what will happen to the weekend work...

Friday, October 26, 2012

Very late Ada Lovelace Day 2012 picture...

"Computing is too important to be left to men"
Karen Sparck-Jones, 2007.

Shieber post

When Margaret Tatcher resigned in 1990, Karen came to my office in the Computer Lab, shared with several other postdocs, excited by the news. Since I was alone in the office in the early morning, she exclaimed, `oh there is no one here' presumably  for her to tell the good news, turn around and left. I started laughing, the news were really cause for jubilation.

Later on we became good friends and I remember fondly a walk in Nancy, after the conference dinner in 2004, talking about computing, linguistics, marriage and children.

Saturday, October 6, 2012

Wayback Machine, I love you! IMLA 1999

I was looking for the data on previous IMLA workshops, as we need to organize the new one, the 6th IMLA, which is happening in Rio de Janeiro, in April 2013, as part of 4th Unilog.

Now the web is vast and things never disappear from it. Unless you want them, that is.

For instance the whole Hypatia archive of pdf papers (kudos to M. Dawson -- I believe-- for creating it in the early nineties) has disappeared without a trace... But I am not going down the rabbit hole of trying to find it. Had enough of rooting around the wayback machine today to find the program of IMLA 1999.

Luckily I did find the IMLA 1999 program and at least one associated page that tells me the program committee and invited speaker. This is enough for one Saturday...

But while I'm at it I must repeat that the Wayback Machine is wonderful. The guys who conceived the Internet Archive and the Wayback Machine and that keep it going are my heroes!

Reproducing the program of IMLA  1999 here to have it easily.

Patent win?...

Two great things happened two Mondays ago:

I started working at Nuance Communications in Sunnyvale, yay!

And my patent with Ji Fang, Jessica Staddon and other colleagues in PARC on detecting sensitive content in documents was granted. (Funny, only got to know about it because the guys who sell you wooden plaques told me...)

Now, I do not like the idea of patents at all.
Probably would prefer if we lived in a world where they didn't exist.

But I feel that during  my years at PARC I contributed to several projects where others got  patents and I didn't, which wasn't fair. So this is very sweet!

Friday, September 21, 2012

From Quirky Case to Representing Space: AnnieFest one year later...

AnnieFest was almost a year ago and I'm pleased to report that because Tracy H. King is such a powerhouse of organization all is well with the volume arising from it.

Listing here the talks, as PARC doesn't keep its pages going for very long...

5 October 2011
George E. Pake Auditorium, PARC, 3333 Coyote Hill Road, Palo Alto, California


This symposium is being held on the occasion of Annie Zaenen's retirement from PARC to honor her significant contributions to theoretical and computational linguistics over a long and distinguished career.
The symposium features speakers who have collaborated closely with Annie at different times and on different topics, representing the broad sweep of her theoretical and practical concerns. The talks and discussion will reflect on their collaborations with Annie and offer new perspectives on language issues of current interest.
Joan Maling, Brandeis University and U.S. National Science Foundation
Chapter 1. Iceland: Is Icelandic a natural language
Joan Bresnan, Stanford University and CSLI
The evolution of syntax in the time of Annie

Hans Uszkoreit, DFKI and Saarland University
Anette Frank, Heidelberg University
Diving into semantics -- and getting hidden meanings out
Livia Polanyi, Microsoft Corporation
Sentiment Analysis and the linguistic structure of Discourse
Geoffrey Nunberg, University of California at Berkeley
L'avis des mots
Danny Bobrow, PARC
Ron Kaplan, Microsoft
Tracy King, eBay
Valeria de Paiva, Rearden Commerce
Sponsored by PARC.

Sunday, September 16, 2012

Constructive modal logics? in the plural?

(picture by Eric Volpe, check his flickr stream)

A long time ago I started compiling a bibliography of work on constructive modal logics. Now I've decided to make it a Google Docs so that people can help me improve it,  adding and correcting things.

Online bibliographies seem to me  a sensible idea.

Saturday, September 15, 2012

Where's the meeting that was cancelled?

When I was still at PARC -- 2008 seems an awful long time ago now -- I invited Patricia Amaral, then a recently graduated research student to come and visit us for a short while. She was applying to be a research assistant in Linguistics, Stanford and being in Palo Alto a little earlier was a good idea. It was lucky that the Gulbekian Foundation agreed too. We wanted to work on improving the system Bridge (about which I will write informally some other day, but an official description can be found in PARC's Bridge and Question Answering System and a personal preliminary take can be found here).

Being a latecomer to computational linguistics and perhaps a bit too optimistic about research, I always have dozens of ideas of things I want to get done, but little ability to predict the time that it takes to get those things done. In this case, however, everything worked well. Patricia got the hang of the system very quickly and soon enough made gigantic progress on the issue I wanted to deal with.

Despite our claims in Preventing Existence (and despite the beautiful algorithm that Rowan, Cleo and Lauri described in Computing Relative Polarity for Textual Inference) the Bridge system could, at that stage, only deal with logical contexts introduced by verbs with a full complement phrase. So something like Ed knew that Mary arrived  would be fine, a logical context would be created with the right polarity, but Ed knew of Mary's arrival  would not create a logical context. (The Bridge system works with full deep LFG parses of sentences and it easier to mark the complemented verbs.)

Thus my goal for the work with Patricia was the extension of the marking of verbs that introduce context, from the ones with full complement to ones that were simply directly transitive.  As usual the problem was much harder than I expected and Patricia, at the end of her stay, gave us a huge presentation with millions of issues and a possible classification that would be a first stab at solving the original problem.

This was written up in a paper  (by Patricia, myself, Cleo Condoravdi and Annie Zaenen) submitted to the workshop on contexts associated with ECAI2008. The paper accepted, but none of us could attend. So we withdraw the paper, hoping to improve it.

Very recently I took the initiative of re-submitting the paper to ONTOBRAS2012 in Recife, Brazil, as I had hoped to go visit some  friends there. But this was not possible, so the paper, again accepted,  had to be withdrawn. Again.

The newly named Where's the meeting that was cancelled? paper seems a bit unlucky, but the work is very cool. Patricia came up with this idea of treating verbs that change  existential commitments as pre and post conditions reminiscent of Hoare's logic. This connection is hinted at in the paper, but not pursued, as the need for classification large-scale was definitely more important then. Someone should work on this, though.

(Meanwhile together with Lottie Price and Tracy King, I worked a little on nouns that introduce logical contexts, cf. Contexts Inducing Nouns.)

Monday, September 10, 2012

Why Constructive Modal Logics?

I guess the question can be taken as both why constructive?, if we like modal logics, but also as why modal?, if we favor constructive logic. (some might even ask why logic at all?, but we won't go there...)

I will try to outline my answers to both forms of the question.

To my functional programming friends, the answer to why modal? goes via extending the  Curry-Howard paradigm to deal with effects, exceptions, I/O and other non-pure features of real-life computations. Despite all the excellent work in this area in the last thirty years or so, the models and tools we have still seem to work best for sequential, effect-free functional programming. The hope is that extending the Curry-Howard to more modal systems will allow us to deal with more of the computing we already do, but are not able to model accurately.

To my modal logicians friends, the answer to why constructive? goes via pointing out the affordances of Curry-Howard as well as the niceties of having an amenable proof-theory with explicit computational content.

 I still believe what we wrote in the preface of the special issue devoted to IMLA in 2004, viz.   `Proofs carry concrete intensional information over and above the fact that a formula is valid. From this point of view modalities come in naturally, viz.\ as syntactic reflections of this underlying intensional level hidden in the proof theory of a constructive logic. A constructive modal logic might arise in an attempt to handle the intensional dimension, or parameter, of modalities (time, nondeterminism, security margin, knowledge, beliefs, etc.) in a computational way at the level of the proof theory. It seems obvious that such a program has much to offer not only from a computer science perspective.'

However I will freely admit that putting together constructivity and intensionality in the guise of constructive modal logics is not an easy task, as there are many design decisions to take and these do not seem clear cut to me. Even the definitions of systems are up for grabs, so there is very little known about semantics and/or complexity results, for instance. Worse still I cannot point out at huge successes in the form of logically-based systems being used in real applications. The best I seem to be able to do is point out at (many though!) systems that use ideas from the Curry-Howard correspondence...

Intuitionistic Modal Logics and Applications (IMLA2013)

For a fair number of years now I have been working on modalities in constructive logics and type theories. This started with the  realization that the Linear Logic "of course" exponential connective corresponds to an S4-box operator (1992), which became my paper with Gavin Bierman On an Intuitionistic Modal Logic, Studia Logica (65):383-416, 2000.

And it has continued ever since in an informal project with many collaborators including Nick Benton, Torben Brauner, Gianluigi Bellin, Eike Ritter, Michael Mendler, Rajeev Gore, Natasha Alechina, Neil Ghani, Milly Maietti, etc.  The main outcome of this project has been the organization of Intuitionistic Modal Logic and Applications (IMLA) workshops and the journal special issues that came from them.

So far there have been 5 such workshops. Now the 6th Workshop on Intuitionistic Modal Logic and Applications (IMLA2013) will be held in association with Unilog2013,  in March-April, 2013 in Rio de Janeiro, Brazil.

Previous workshops were part of FLoC1999, Trento, Italy, of FLoC2002, Copenhagen, Denmark, part of LiCS2005, Chicago, USA, part of LiCS2008, Pittsburgh, USA and part of the 14th Congress of Logic, Methdology and Philosophy of Science, Nancy, France, 25 July, 2011.

I wasn't much associated with the first workshop in Trento, but have been involved in all the others. Three special issues of journals have been published from IMLA workshops so far (a fourth is being produced, editors Natasha Alechina and me):

  1. M. Fairtlough, M. Mendler, E. Moggi (eds.): Modalities in Type Theory. Mathematical Structures in Computer Science, Vol. 11, No. 4, August 2001.
  2. V. De Paiva, R. Gore, M. Mendler (eds.): Modalities in Constructive Modal Logics and Type Theories. Special issue of the Journal Logic and Computation, editorial pp. 439-446, Vol. 14, No. 4, Oxford University Press, August 2004.
  3. Valeria de Paiva, Brigitte Pientka (eds.): Intuitionistic Modal Logic and Applications (IMLA 2008). Inf. Comput. 209(12): 1435-1436 (2011).

Tuesday, September 4, 2012

Ideas to discuss with Elaine?

Elaine wanted to discuss some more mathematical ideas that she might (or not) want to talk to her students about. Sitting in the several planes that it took me to get home, I made a preliminary list of things that I wanted to talk to her about.

#1. Dialectica categories relationship to Milner's "tacticals", in Budiu et al's partial compilers paper. Also relationship to sub-exponentials, as Dialectica categories have three notions of modalities.
#2. Hopf (co)-algebras in Dialectica categories (Blute/Majid?).
#3. Prove (using TATU perhaps?) cut-elimination for FILL. I guess this is hard, given what she said about multiple-conclusion versions of IL.
#4. Proof-theoretical institutions. Why my work with Rabe et al  is not good enough. as far as I'm concerned, that is.

Wednesday, August 22, 2012

Playing with models, again...

Gavin Bierman wrote a very clear paper "What is a Categorical Model of Intuitionistic Linear Logic?" in 1995. Andrea Schalk has some detailed notes on her web page "What is a Categorical Model of Linear Logic?" Paul-Andre Mellies has two versions "Categorical models of linear logic revisited" (2003) and "Categorical Semantics of Linear Logic" (2012).  Together with Milly Maietti, Paola Maneggia and Eike Ritter, I have Relating Categorical Semantics for Intuitionistic Linear LogicBy myself I have Categorical Semantics of Linear Logic for All, which needs some cleaning up and updating in places. Why do we need so many? Need to write a post with preliminary conclusions.

Tuesday, August 14, 2012

Paraty is drawing closer...

As usual, things got a bit delayed, so I have no slides, yet, for Proof Theory 2012. But I know I'm staying at "Pousada Villas de Paraty" and I have a ticket. so far, so good.

I also got invited by Jean-Yves Beziau to talk at Logic in Rio, so need to think about that too.

I now have a title "Who's Afraid of Categorical Models?" and a minimal abstract. Have decided to revisit a manuscript from 2006 "Categorical Semantics of Linear Logic For All", kind of the reason why I called this blog "Forro' Logico".

Wednesday, August 8, 2012

Bib Woes

Need to discover what is written in our these papers/notes below. And need to decide what to improve and how to go about it...

Update: Just re-read this and should explain that I actually have helped writing these papers... :)

It's just that I get confused on which one is which and I don't think I have final versions of them all, so what I mean is that I need to get final versions out of gmail/dropbox/etc... and try to map out a way to carry on with this project.

the papers are:

de Paiva, Valeria, and Alexandre Rademaker. 2012. “Revisiting a Brazilian WordNet”. In Proceedings of Global Wordnet Conference. Matsue: Global Wordnet Association.more

Haeusler, Edward Hermann, Valeria de Paiva, and Alexandre Rademaker. 2011. “Intuitionistic Description Logic and Legal Reasoning”. In XVI The Brazilian Logic Conference. Petrópolis.more

Haeusler, Edward Hermann, Valeria de Paiva, and Alexandre Rademaker. 2011. “Intuitionistic Description Logic and Legal Reasoning”. In 2011 Database and Expert Systems Applications, DEXA, International Workshops. Toulouse: IEEE Computer Society. doi:10.1109/DEXA.2011.46.more

de Paiva, Valeria, Edward Hermann Haeusler, and Alexandre Rademaker. 2011. “Constructive Description Logics Hybrid-Style”. Electronic Notes In Theoretical Computer Science 273: 21–31.more

Haeusler, Edward Hermann, Valeria de Paiva, and Alexandre Rademaker. 2010. “Using Intuitionistic Logic As a Basis For Legal Ontologies”. In Proceedings of the 4th Workshop On Legal Ontologies and Artificial Intelligence Techniques. Fiesole (Florence): European University Institute.more

Haeusler, Edward Hermann, Valeria de Paiva, and Alexandre Rademaker. 2010. “Using Intuitionistic Logic As a Basis For Legal Ontologies”. Informatica E Diritto (Journal On Informatics and Law) 1: 289–298.more

Haeusler, Edward Hermann, Valeria de Paiva, and Alexandre Rademaker. 2010. “Intuitionistic Logic and Legal Ontologies”. In Frontiers In Artificial Intelligence and Applications. Amsterdam: IOS Press. doi:10.3233/978-1-60750-682-9-

de Paiva, Valeria, Edward Hermann Haeusler, and Alexandre Rademaker. 2010. “Constructive Description Logic, Hybrid-Style”. In Pre-Proceedings of International Workshop On Hybrid Logic and Applications. Edinburgh.more

Sunday, August 5, 2012

Resources and Reasoning: a new project?

Actually, it is the continuation of "Logics and Ontologies for Portuguese" which started in July, 2011.
Resources & Reasoning has three main goals:
1. Measure and  improve the accuracy of OpenWordNet-PT;
2. Choose and implement a version of named entity recognition for Brazilian Portuguese;
3. Demonstrate the feasibility of a prototype for reasoning about relationships between historical characters in the DHBB, using SUMO-Sigma and the resources we have created.

Writing research projects is hard work, as you don't want to promise too much and not live up to people's expectations. But you also do not want to promise too little and risk people not getting excited about the project at all. Finally there some bits that even if not the most exciting things, need to be done so that you do get to the exciting ones and you must try to show some enthusiasm for these boring bits too.

Wednesday, August 1, 2012

More on Logics and Ontologies for Portuguese

It's  rather annoying that all my photos of the meeting at Thanksgiving last year at FGV in Rio seem to have disappeared. Must write to Alexandre and Gerard and ask about theirs. Meanwhile just to facilitate my blog-navigation here's the link to the place where I try to keep information about natural language adventures.

I'm really chuffed with Francis Bond search interface to a collection of WordNets, including our OpenWN-PT,  and have to stop myself playing with it. Must  focus on the work that I need to get done. but yeah, maybe I should write down all the exciting possibilities I see for it, before I forget them...

Update: got some pictures from Alexandre, who's visiting California, yay.

Sunday, July 29, 2012

Existential Change Verbs?

If you find a sentence like "Our reservations were cancelled by the hotel computing system" you need to know that, whether you name them or not, whether you're using bag-of-words or not, someone's reservations do not exist anymore in that hotel.

Patricia Amaral, Cleo Condoravdi, Annie Zaenen and I worked a little on the problem of classifying verbs that exhibit this "existential change" effect. We submitted a paper to a context workshop in 2008, it was accepted, but no one had time to travel for that conference. Now we submitted it again to ONTOBRAS-MOST 2012 in Recife.

Friday, July 27, 2012

OpenWN-PT is online!!

Together with Alexandre Rademaker and Gerard de Melo I have been working on a version of WordNet for Portuguese that is open, downloadable and modifiable by all. The paper was called "Revisiting a Brazilian WordNet" and it appeared in the Proceedings of Global Wordnet Conference.

We call it OpenWN-PT because there are some other efforts at Portuguese WordNets, including the MultiWordNet-Portuguese, the Portuguese Wordnet of P. Marrafa and the Brazilian Portuguese WordNet of Bento Dias-da-Silva. Ours is small, but downloadable and improvable.

This week we heard from Francis Bond that this has been incorporated into Francis' project,  Open Multilingual Wordnet (link below) which makes it online, searchable and "linked" to SUMO, which I worked on with  Adam Pease.

YAY!!! Great news guys, many thanks!!!

Open Multilingual Wordnet


Tuesday, July 24, 2012

Language and Natural Reasoning

Annie has created a new group in CSLI, Language and Natural Reasoning.

I guess I need to justify my participation, so I need to write up my RAIN (Reasoning and Interaction as NASSLLI) talk: Little engines of Inference: Contexts for Quantification.

Women in Logic? Yes!

Catarina Dutilh Novaes had the clever  idea of making a list of women working in logic.

But the list was not alphabetical (which made it difficult to know if you were in there) and it had no webpages for the women there (which made it difficult to read their work).

So I've asked Anna Crouch to find out the webpages for the women in the list and to make it  alphabetical

Ruth Barcan Marcus in 1943 and a "year of zipping and unzipping snowsuits" to illustrate.

Sunday, July 22, 2012

Fuzzy Sets in Brazil

Apostolos Syropoulos and I have managed to submit a paper  on (Dialectica-style) Fuzzy Topological Systems for the

II CBSF - Second Brazilian Congress on Fuzzy Systems


Thanks Elaine Pimentel for the photo of Natal!

Computing in Tunisia?

 Prof. Fairouz Kamareddine (Heriot-Watt University, Edinburgh, UK) invited me to the program committee of this new conference in Tunisia,

International Symposium on Symbolic Computation in Software Science,
December 15-17 2012
Gammarth, Tunisia

I sure would like to go to Tunisia.

August 23, 2012: Paper title and abstract deadline
August 30, 2012: Full paper deadline (firm)
October 30, 2012: Author notification
November 30, 2012: Final version deadline (firm)
December 15-17, 2012: Symposium

Friday, July 20, 2012

Lambek Calculus and Dialectica Categories

Many years ago I wrote a short note on a categorical model of the Lambek Calculus using the Dialectica construction. The note is imaginatively called A Dialectica Model of the Lambek Calculus.

This is interesting for a couple of reasons. First because the original dialectica constructions are all commutative and the Lambek calculus is definitely not commutative.
Second because the route I took to start from the Lambek calculus and end up in classical propositional logic, I have not seen taken since. It was based on previous work of Yetter and independently Morrill-Hepple-Moortgat and it's surprising to me that others have not decided to use it.

 I talked about it at both the Durham Symposium and the Amsterdam Colloquium. But with job moves, house moves,  broken computers and passwords-that-don't-work, I had not a single copy of my own paper. So I wrote to the nice guys in Amsterdam and thanks to wonderful Peter van Ormondt, Paul Dekker, Maria Aloni and Johan van Benthem I now have at least a scanned copy of  Peter's volume. Thank you guys!

So if like me, you want to read it, you can check it out at the place provided by the also nice guys  at Slideshare. Google Docs doesn't allow you to upload a 3.5MB scanned file, but Slideshare does. On the other hand, I did have a postscript/pdf  draft version that might be easier to read.

Wednesday, July 18, 2012

Kinds of Categorical Fuzzy Sets

In the logic seminar in Stanford sometimes people are asked to present papers. That's how I ended up reading Takeuti and Titani on fuzzy sets, which turned to be very interesting.

Now I'm reading Gottwald on "Universes of Fuzzy Sets and Axiomatizations of Fuzzy Set Theory. Part II: Category Theoretic Approaches" and this is very interesting too, for the same reason.

I have known since around  1990 that I can construct a "fuzzy" version of dialectica categories.  I know that this construction gives us a symmetric monoidal closed category with products and coproducts, with a (admittedly complicated) linear exponential comonad, hence is a model of Linear Logic. I know that there are other fuzzy sets that are also models of Linear Logic. Presumably I can relate these models via functors.

 I have not managed, so far,   to discover what makes fuzzy logic such a "crowd-puller", such a strong favorite. so I have no idea if this attractiveness will hold for the linear logic models. Or not.

Tuesday, July 17, 2012

Reading about Univalent Foundations

Voevodsky’s proposal to the NSF and IAS(2010) consists of 13 pages. The slides from his talk in Goteborg (Sept 2011) are easier to understand. Both can be found  in the univalent foundations page.

There is also the page on Homotopy Type Theory tout court, with more information on other researchers' views. 

Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory.  Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. Slides from Thierry Coquand following this kind of explanation in Oberwolfach are  linked from here.

The original work that is the basis of this stuff is the groupoid model of Martin-Loeuf's CTT by Thomas Streicher and Martin Hofmann, here.

The broad motivation behind univalent foundations is a desire to have a system in which mathematics can be formalised in a manner which is as natural as possible. Whilst it is possible to encode all of mathematics into Zermelo-Fraenkel set theory, the manner in which this is done is frequently ugly; worse, when one does so, there remain many statements of ZF which are mathematically meaningless. This problem becomes particularly pressing in attempting a computer formalisation of mathematics; in the standard foundations, to write down in full even the most basic definitions—of isomorphism between sets, or of group structure on a set—requires many pages of symbols.

Univalent foundations seeks to improve on this situation by providing a system, based on Martin-Loef’s dependent type theory, whose syntax is tightly wedded to the intended semantical interpretation in the world of everyday mathematics. In particular, it allows the direct formalisation
of the world of homotopy types; indeed, these are the basic entities dealt with.

Constructing a model of the univalent foundations in the category of simplicial sets Voevodsky shows the consistency of these foundations relative to the usual ones. But this is just a first sanity check, if the new foundations are to be used, what do we need to know about them?

Some highlights of the Voevodsky proposal (first pages only).
  1. We're close to "a new era which will be characterized by the widespread use of automated tools for proof construction and verification". yeah.
  2. V came up with "a new semantics for dependent type theories - the class of formal systems which are widely used in the theory of programming languages"    Cool about the new semantics. I wish the bit about 'widely used' was true.
  3.  "univalent semantics" interprets types as homotopy types. "the key property of the univalent interpretation is that it satisfies the univalence axiom a new axiom which makes it possible to automatically transport constructions and proofs between types which are connected by appropriately defined weak equivalences."    ok, need definitions...
  4.  The key features of  "univalent foundations":
  •  axiomatization of n-categorical structure
  •  language is dependent type theory
  •  based on homotopy types, not sets
  •  both constructive and non-constructive maths

Univalent Foundations? Go Voevodsky!

 I should be an awful lot better at explaining hard stuff than I am.  This is because before starting mathematics I had one year of journalism and half a year of law in college. Long story, don't ask.(oddly enough, this hasn't helped me much.)

But since I am not good at explanations and I would like to improve, I've decided to write down (over)simplified versions of ideas to see if "practice makes perfect". I've decided to start with Vladimir Voevodsky's programme on Univalent Foundations for Mathematics.

There is a couple of reasons for that. First it's one of the more interest-generating new ideas in Category Theory. Some of it it's just because Voevodsky is a Fields medallist and all that. Some is because category theorists have a "chip on their shoulder" as far as other branches of mathematics are concerned. Despite claims in Wikipedia (of all places) that  abstract nonsense is a term of endearment, true category theorists know that it's not. It's an insult where more established branches of mathematics want to say that what we do is just dress up old concepts in new language. But thirdly and far more importantly the reason for trying to explain (to myself) what Univalent Foundations is about is that fact that this is the first serious attempt to extract new mathematics from the Curry-Howard isomorphism.

Why does this matter, do you ask? Well, the Curry-Howard iso is something that I've been trying to explain (to myself and others) for the last twenty years and I still haven't got a good way of doing it. So I wanted to use this non-serious medium (I cannot be corrupting the youth or damaging anyone else's reputation in a blog post) to try out a few off the wall ideas.

One of the things that makes explaining other people's work hard is that your own work and ideas keep trying to introduce themselves into the explanation. One has to fight to keep them off. The case of univalent foundations is slightly easier for me, as my own work is very marginally related to them. 

Monday, July 16, 2012

More on why Infinite Possibilities was so cool..

The Infinite Possibilities Conference (IPC) is a national conference that is designed to promote, educate, encourage and support minority women interested in mathematics and statistics.

The conference is important because African-American, Hispanic/Latina, and American Indian women have been historically underrepresented in mathematics. In 2002, less than 1% of the doctoral degrees in the mathematical sciences were awarded to American women from underrepresented minority groups. Even professionals who have succeeded in completing advanced degree programs in science and engineering fields can face inequities within their professional lives with respect to advancement and salaries. 

 In 2012 IPC was called "Building Diversity in Science and Mathematics", it happened 30-31st March at the University of Maryland, Baltimore County, Baltimore, MD and I had the honor of being one of the two keynote speakers. Many of the mathematicians I met there seemed to be working with mathematical Biology,  I was the only speaker talking from a Computer Science,  programming languages perspective.

My talk was entitled ``Edwardian Proofs for Futuristic Programs" and besides the required description of my career path so far,  talked about the birth of Mathematical Logic in the early years on the 20th century and how Proof Theory, one of the main strands of Mathematical Logic got a big impulse via the advent of Computing for all, through the (still today!) poorly recognized Curry-Howard Isomorphism and its more mathematical incarnations. 

This is a difficult talk to give, even for people interested in Computer Science, let alone for a generic mathematical audience. So I reckon I need to keep working on making it more accessible. It's a tall order, as Category Theory seems to scare people off, even mathematicians. The slides are available here, if you want to have a look.

Sunday, July 15, 2012

Paraty 2012

I've been invited to give a talk at
Proof Theory: Linear Logic, Ludics and Geometry of Interaction. 

The link is here, but I don't think there's much information there, yet.

Saturday, July 14, 2012

Intuitionistic Modal Logic and Applications 2011 Nancy, France

Natasha Alechina and I organized this meeting on

Intuitionistic Modal Logics and Applications Workshop (IMLA'11)

as part of the 14th Congress of Logic, Methdology and Philosophy of Science in Nancy, France, 25 July 2011.

The webpage is in the Agents Lab in the University of Nottingham and the call for papers for the publication after the meeting is here.

Sunday, July 8, 2012

Party at NASSLLI?

GetFUN good news

So I have been helping to write a twinning logic research project between Brazil and Europe, in the shape of Portugal, Italy, Romania and Israel(!?...).

Just heard that it has been accepted, yay!
Great job Carlos Caleiro and Joao Marcos!

Tuesday, July 3, 2012

Thursday, June 28, 2012

Back from NASSLLI

NASSLLI2012 was great, too many great courses to follow, too many interesting people to chat to, too little time to do everything.

Now I realize that I haven't been paying any attention to recording/collecting stuff that I have been doing and, age being what it is, I forget what I have done. and also what I have not done yet...

so I will try another round of blog-post-its, in the hopes that when I finally get my Bham account unlocked and my G'sites account working, life will be easier.

First off: Jean-Yves Beziau and Marcelo Coniglio organized a book in honor of Walter Carnielli's 60th Birthday. I did manage to get a paper on constructive modal logic in, yay!

Monday, June 18, 2012

Homework 2?

Check this short homework out. Slides after the class.

Category Theory for all, June 18, 2012

The slides for today's lecture are here.

Hopefully a not-crazy-jumping pdf, but instead one that you can go up and down, at your leisure.

Thanks for the patience with the scrolling issues!
And  thanks for the expert diagnostics after the event.

Please do take a look at the post on  references for introductions to Category Theory, if you can. 

Sunday, June 17, 2012

Categorical Proof Theory and Linear Logic

These are some very, very old notes from a course I gave in Prague, at  ESSLLI 1996.

The idea was to present enough basic category theory and enough basic proof theory to discuss the categorical modelling of Linear Logic and ... drum roll...introduce  Dialectica Categories.

(and yes, I also had high expectations of understanding enough about models of Linear Logic to be able to discuss them all and write a book, ha...)

 Now I have reduced my expectations and I simply would like to introduce enough category theory to make the categorical modelling of Intuitionistic Logic plausible (before I wanted to do both intuitionistic and linear logic).

But in compensation I would like to do this in four lectures only, as I wanted to keep the 5th lecture to introduce Glue Semantics,  in the style that a linear logician, especially  a budding one, would understand it. At least this is the plan.

Homework for Cat Theory Day 1: why not?

So you know, I hope, that mathematics is not an spectator's sport.
You need to do the calculations, otherwise the stuff doesn't work.

The good news is that no one will come after you, asking for your grades or anything like it. And that you can come and ask  me questions, if you feel like it.

The bad news is that, if you don't do them (the exercises) you'll end up thinking that you've learnt and sometimes you haven't. Your call, of course.

To sweeten the pill, there's a reading for each day, just for the fun of it.
For the exercises, there are answers on the web, but you should really try to do it, first.

The first treat is “The aims of Education” by Andrew Abbott of the University of Chicago. Only 5 pages and (I find it) a different take on why do we go to college.

Thursday, June 14, 2012

Mathematics as we know it...

Frank Quinn had a very interesting article entitled "A REVOLUTION IN MATHEMATICS? WHAT REALLY HAPPENED A CENTURY AGO, AND WHY IT MATTERS TODAY", in the Notices of the AMS, January 2012. You can find it it in his education webpage.

Living and Learning?

Category Theory requires exercises, so I'm trying to organize homework sheets. But I want to add some treats to the homework, a bit like I a did for Phil50/COEN260.

The first treat is “The aims of Education” by Andrew Abbott of the University of Chicago. Only 5 pages and (I find it) a different take on why do we go to college.

The second treat is Lockhart's Lament, check this old post.

The third treat is Quinn's Revolution, published by the AMS, January 2012.

The fourth treat is  Anonymous in Quora on  "What is it like to have an understanding of very advanced mathematics?"

We end with something different, Eli Pariser on "The Filter Bubble", TED talk, May 2011.

And yes, I feel sorry not to include Wigner's `The Unreasonable Effectiveness of Mathematics in the Natural Sciences'. Nor Hamming's ``The Unreasonable Effectiveness of Mathematics" and perhaps the unreasonable effectiveness of data should be mentioned too...

Oh well too many treats might make us sick...
But keeping links in store is not so bad, shame I don't seem to find "The Canon of Technology" anymore.

Category Theory introduction? yeah, sure...


There is plenty of material on category theory around. Collecting here some old favorites and some newer stuff that I haven't checked out,  yet.

The familiar:
S. Mac Lane, Categories for the Working Mathematician (1971, 1998)

R. Goldblatt, Topoi, Dover reprint and online (1979, 1984, 1986, 2002).

J.-Y. Girard, Y. Lafont, P. Taylor, Proofs and Types (1989) online 

V. de Paiva, Categorical Proof Theory and Linear Logic, ESSLLI, Prague (1996) google doc sideways(!) available

D. Crouch, J. Genabith, Linear Logic for Linguists, ESSLLI (2000), notes

J. Gallier, Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi, paper

Then some traditional fare:

R. Blute P. Scott, Category Theory for Linear Logicians (2003)

F.W. Lawvere, S.H. Schanuel, Conceptual Mathematics (1997)

S. Awodey, Category Theory, (2010)

H. Simmons, An Introduction to Category Theory, CUP, (2011) online version

Adámek, Jiří, Herrlich, Horst, & Strecker, George E.; (1990). Abstract and Concrete Categories Originally publ. John Wiley & Sons. ISBN 0-471-60922-6. (now free on-line edition). 

M. Barr, C. Wells, Toposes, Triples and Theories, 1983, now online.

Then more adventurous (perhaps??) stuff:

M. Johansson, Category Theory and Functional Programming, Stanford FALL 2009 course and St. Andrews 2012 notes   (99 pages)

also Chalmers discussion group

Abramsky and Tzevelekos, "Introduction to Categories and Categorical Logic" (2010)
G. Hutton, Introduction to Category Theory, Midlands Graduate School notes, 2012.

D. Verity, An Introduction to Category Theory - FP-Syd talk.

E. Cheng, The Catstars, YouTube channel.

J. van Oosten, Basic Category Theory, 2002, notes

L. Maertens, Category Theory for Program Construction. ESSLLI notes (1995)

S. Easterbrook, An introduction to Category Theory for Software Engineers, slides

Further afield:

  • Sets for Mathematics by F. W. Lawvere & R. Rosebrugh.
  • Topoi: The Categorical Analysis of Logic by R. Goldblatt.
  • Abstract and Concrete Categories: The Joy of Cats by J. Adamek, H. Herrlich, G. Strecker.
  • Categorical Logic by A. M. Pitts. 
  • Stone Spaces by P. T. Johnstone.
  • Sheaves in Geometry and Logic: A First Intorduction to Topos Theory by S. Mac Lane & I. Moerdijk.
  • Handbook of Categorical Algebra (three volumes) by F. Borceux.

Sunday, June 3, 2012

Categorical Logic Lab? Yes!!!

The bit I saw of the Logic, Rationality and Interaction meeting was excellent.
Love the idea of logical labs:  I want a Categorical Logic Lab!
How do I go about getting one?...

Saturday, June 2, 2012

March was Qualis Time

no, not quality time. (haven't had that for ages...)

QUALIS is the system CAPES (a Brazilian funding agency) uses to measure the quality of pos-grad programmes. Since they classify journals, it ends up being an unofficial yardstick to measure all research produced in the land. Some Brazilian logicians realized that the classification was very arbitrary and we had a petition to try to influence the official arbiters.

Getting a petition going and some small amount of consensus on the classification of journals was very hard.

XV Simposio Latino Americano de Logica Matematica (SLALM2012)

Going to Bogota, Colombia today for the 15th Latin American Symposium on Mathematical Logic.
A bit worried as I don't know many people in this community, but looking forward. 

Sunday, May 27, 2012

Lua at Rearden, 14 March, 2012

Roberto was Tinker Professor in Stanford at the beginning of the year, which was wonderful. Had great dinners with Noemi, Roberto  and Ana Lucia and when the girls went home, had several other opportunities to drink wine and talk shop with Roberto. I would like to know more about Lua.

So I invited Roberto to give a  Rearden University presentation in March. His abstract, with a link to his slides.

About Lua

Lua is a programming language developed at the Catholic University
in Rio de Janeiro that came to be the leading scripting language in
video games. Lua is also used extensively in embedded devices, such as
set-top boxes and TVs, and other applications like Adobe Lightroom and
Wikipedia. In this talk we will see where Lua is being used, why Lua is
being used, and what makes Lua special.

Roberto Ierusalimschy is Associate Professor at the Pontifical Catholic
University in Rio de Janeiro (PUC-Rio) and the leading architect of the
Lua programming language. Currently he is a Tinker Visiting Professor
at Stanford.

They're having their workshop this November at Verisign.