Our Grant Money of Every Day

I have a long history of getting grant money that I cannot use, because I have moved, or because the partner changed his/her mind, etc.

It started with the project "Authentication Logics", which I mostly wrote for co-P.I's Larry Paulson and Roger M. Needham in 1995. Larry had been my sponsor in the previous project on "Evaluation Logic" with Andrew Pitts and I was really grateful when he accepted the idea of a project on authentication logics and invited Prof. Needham. I was also grateful to Kim Wagner, who stepped in to be the RA, when I was offered a proper lectureship in Birmingham and moved there in January 1996.

Of course they changed completely the direction of the project, which was about theory and implementation in Isabelle and ended up being about a new method in Isabelle, i.e. a totally different, but quite interesting new theory and mostly its implementation.

Larry's project  page, linked above, says:

Authentication Logics:
New Theory and Implementations

Lawrence C. Paulson and Roger M. Needham (with thanks to Valeria de Paiva)

Research associates: Kim Wagner (to 31 March 1997), Katherine Eastaughffe

Funded by the EPSRC (1 Jan 1996 to 30 June 1999). Grant reference GR/K77051. Value £157,244

This project developed the inductive approach to verifying cryptographic protocols. The key paper has been cited over 1100 times.

In distributed computing systems, components of the system (people, computers, services: usually called principals) must satisfy themselves mutually that they are who they say they are. This is the reason for authentication protocols. Formal analysis of these protocols is highly desirable for discovering flaws and omissions.

This proposal concerns the study of authentication logics, a widespread formal method used in the verification of security protocols. We make a case for a deeper theoretical analysis of the method, as well as for implementations of the resulting logics in the generic theorem prover Isabelle. In the course of the work, attention has shifted from authentication logics to new methods based upon operational models and inductive proofs.

Sets, Types and Categories

Joao Marcos managed to establish, quite a few years ago now, a Brazilian mailing list of logic and logicians. This can be very useful at times. (Some times I just despair of humanity. But this is the essence of mailing lists, I suspect.)

Anyways there was a good discussion over the Christmas break and I thought I should summarize it here for my own future benefit.

The discussion started with JM pointing to a question on some unsolved problems in mathematics. The answers were not about mathematics, but about Set Theory and Andrej Bauer had a pithy comment, as pointed out by Vivek Nigam:
"Logic of the early 20th century was a reaction to a conceptual and methodological crisis in mathematics. Logic of the early 21st century is the tool for conquering the newly discovered land of computer science. Now is a good time to be an Edison or a Tesla of logic, and a little less a Cantor or a Russell. (It's always good to be a Gödel or a Turing, of course.)"

I commented that it's always good to be some one like Cantor or Russell (captain-obvious that I am) and that, despite liking Andrej and logic in computing very much, I  thought he was being too narrow-minded with this observation, as logic is going plenty of other places too.  Mind you, I have talked about computing being the physics of this century in several places, as far as questions, challenges and theories in mathematics goes. So I'm not disagreeing with Andrej, only saying that he should've gone further.

Because I was having a different discussion in facebook, I posted a link to MacAllester's post on a new foundation for mathematics, saying that I disagree with his solution very much, but that people in the list may find it interesting (it's the kind of discussion to have after too much good food and wine, I say). Decio Krause asked me why. I recalled Vijay Saraswat's description of the issue:

(a) One is looking for a framework for mechanically checkable mathematics, much in the way Coq can be used to mechanically check proofs of correctness of various algorithms. (e.g. various theorems related to semantics of programming languages or properties of type systems). (b) A starting point is Martin-Lof's (constructive, dependent) type theory. (c) The underlying notion of type in this framework has proven hard to pin down mathematically. (d) Homotopy theory is claimed to provide some mathematical understanding of types. (e) Hence the enormous interest in HoTT amongst logicians and theoretical computer science (semantics) folks. (f) David is trying to develop a similar framework but based on classical rather than intuitionistic ideas, he wants to retain  the power of "Platonic" worlds and reasoning.

and explained that I agree with MacAllester that there might be a need for a new foundation, but then I don't like his solution.

But then something interesting happened, JM posted a link to Tom Leinster's Rethinking Set Theory, which is pretty impressive. To me at least. Looks sane and sensible, I like it a lot.

I  posted Steve Awodey's From Sets to Types to Categories to Set and lots of discussion ensued. Steve starts his manifesto with:

Three different styles of foundations of mathematics are now commonplace: set theory, type theory, and category theory. How do they relate, and how do they differ? What advantages and disadvantages does each one have over the others? We pursue these questions by considering interpretations of each system into the others and examining the preservation and loss of mathematical content thereby.

Forced by Decio's question "Valéria, Será que o autor consegue falar algo que não saibamos?" I had to read it, which was good as I was thinking about the subject in any case, given the beautiful write-up that Samuel just produced on our work on categorical understanding of set theoretical cardinalities of the continuum.

So here are my own personal preliminary conclusions, half-translated from Portuguese.

Just til page 11 I knew the constructions that make up his "triangle". Thus what is new to me, who hadn't stopped to think about the consequences of the functors in the triangle, are his conclusions in section 5. Awodey says:

1.The first and most obvious conclusion to be drawn from this is that the three systems of foundations are therefore mathematically equivalent.[...] This is perhaps the definition of the “mathematical content” of a system of foundations, i.e. those definitions, theorems, etc. that are independent of the specific technical machinery, that are invariant under a change of foundational schemes.

yay, this works for me!!

2.the objects of type theory and set theory are structured by the operations of their respective systems in certain ways that are not mathematically salient.[..] Categorical structure is closer to the mathematical content, and it is not lost in translation. Equivalence of categories preserves categorical properties and structures, because these are determined only up to isomorphism in the first place.[..] The structural approach implemented by category theory is thus more stable, more robust, more invariant than type or set theoretic constructions. 

Again I like it a lot! This of course does not solve all my problems, all three vertices  of the triangle have their own problems and challenges. 

E da minha parte, como "brinco" entre a teoria de categorias e as `type theories' da vida, as vezes tendo pra um lado, as vezes pro outro. Por exemplo no Unilog de 2005, (junto com a entao minha research assistent Milly Maietti que e' super fan de type theory), eu defendi uma posicao mais pra TT na competicao de como devemos definir logicas. Naquela altura eu estava dizendo que o que a gente precisa 'e de uma sintaxe forte que prove "internal language theorems" pra gente. Mais recentemente venho dizendo que talvez seja melhor firmar sua intuicao nas categorias, pois a sintaxe a gente acaba acertando... Nao sei, nao tenho certeza. 

Como eu acredito na conclusao de que essas coisas sao mesmo "mathematically equivalent"  posso trabalhar tranquila com o Samuel no universo dele que tem Choice(de todo tipo), tem elementos, tem infinitos completos, o escambau.

Anyways, I think the whole episode was very productive, despite a few mishaps. And I would like to thank JM, Decio, Rodrigo for all the knowledge imparted.

books, rejections and carrying on

There are days that you need to pat yourself in the back to try to remember  that things will be all right in the end. Four papers rejected before the end of July is a high rejection rate.

Modal logic, FILL cut elimination and Lean Logic I have been  able to recover from: re-organizing things, re-submitting and getting clearer. Google POS-tags less so and it is so important, oh dear.

The issue is not the rejection, but how to learn and improve from that.

But I had three meetings organized this Summer and all have been successful. WOLLIC's book is pictured, NLCS had a good turn out, despite being so far away and  the Workshop in Barcelona was fun and very productive.

I also gave a collection of invited talks. Yes, definitely a sign that I am old. I knew I was going to talk at CoCoNat and LSFA, I ended up talking also at the Berkeley Colloquium (thanks Wes!), at Stanford's Rationality Workshop (thanks Johan!), at IBM Research (thanks Alexandre!)

Talking much, not calculating enough?

This was another year of talking a lot. First I gave a talk about Intuitionistic Modal Logic in the Logic Colloquium in Berkeley,  on March,  6th 2015, invited by Wes Holliday.

The title was `Constructive Modal Logics: 15 years later'  and it was fun and scary. I thought they had the slides on their page, but now I cannot find them, so the slideshare link will have to suffice.

Then I was invited speaker at 4th CSLI Workshop on Logic, Rationality and Intelligent Interaction, CSLI, Stanford University.  I talked about Lean Logic and the paper is not written, yet.

For this invited talk there are two videos, which really makes me nervous. But on the day I actually felt pretty good about it.

 

Then there was WOLLIC 2015 and I was invited speaker at CocoNat at Indiana University, Bloomington, Indiana. Doing WOLLIC was really hard work, but I am  pleased with the way it turned out in the end. Lots of fun and a serious program. At CoCoNat I talked again about Lean Logic, but I was disappointed that I did not manage to make much progress between the two talks.

Then I was Invited Speaker at LSFA2015 in Natal, RN, Brazil . This was a special present from Elaine Pimentel and I am really grateful. I talked about modal logic again, but this was very different from Berkeley or the paper with Charles and Natasha.  I had seen a message saying that videos were online, and indeed just found them now. Mine is here.

The meeting was great. Huge and really fantastic! Lots of attention to many details, energetic and helpful young ones everywhere,  good talks inside and outside the lecture rooms. I loved it! I also loved their logo, clever and pretty!

The last invited talk of the year was at IBM Research Rio, in September 2015, when I talked about 

Portuguese Linguistic Tools:What, Why and How. 
The view was beautiful and the discussion very good.

This year I was also invited to something very special: to help evaluate the INRIA program on "Proofs and Verification". A very different learning experience.