K for Kripke

I met Saul Kripke only once, when we were invited speakers at  the first Unilog in 2005. Jean-Yves Beziau organized for Mike Dunn and myself to go to the airport with Kripke. In the check-in desk in Geneva, Kripke was the first person I have ever heard of to truly answer the question: Have you been given anything here?  To which he replied that he had been given two books in his honor. Of course this stopped all the check-ins in the airport, as someone was sent down to retrieve his suitacase from the rolling conveyor so that authorities could check that there were indeed two books in his honor and nothing else...

But I digress. There is a very interesting and long discussion going on in Google+ about "necessity and possibility".  I plan to spend some of the weekend reading it properly.

But the reason for this post is that yesterday we had BACAT and I talked about constructive modal logics, once again. I  tried to discuss three old papers:

On an Intuitionistic Modal Logic (with Bierman, Studia Logica 2000)

›Computational Types from a LogicalPerspective (with Benton, Bierman, JFP 1998)

›Basic Constructive Modal Logic. (with Ritter, Logic without Frontiers: Festschrift for Walter Carnielli, 2011)

 The conversation was good, we talked a little about applications to security and to FRP (Functional Reactive Programming) which I need to know more about. 

A quote from Russell, that starts the excellent history of Modal Logic, written by Rob Goldblatt,
Mathematical Modal Logic: a view of its evaluation.


...there is no one fundamental logical notion of necessity, nor consequently of possibility. If this  conclusion is valid, the subject of modality ought to be banished from logic, since propositions are simply true or false...

Slides from the talk are here.