One very cool aspect of this event was that its topic is Linear Logic and it took place in Lyon. Linear Logic was invented by Jean-Yves Girard in 1986 who was born in Lyon. So the location of the event was prefect. The event was also well attended. The participant list contains 106 entries, and during the Linear logic, mathematics, and computer science workshop I did a quick count of 90 people in the room.
Since I was going all the way to France I thought why not make the best of it, and so decided to attend the fall school. It was very well put together. The lectures assumed zero knowledge of linear logic, and began with a very nice introduction by Jean-Baptiste Joinet, and was followed up by Olivier Laurent (slides) who discussed multiplicative-additive linear logic (MALL). I was particularly excited about Olivier’s lecture, because he introduced the concept of proof nets.
One interesting thing to note is that the school concentrated on classical logic instead of other flavors such as intuitionistic logic. In addition, the school presented the logic in a single sided formulation. That is, instead of a sequent like \[A_1,\ldots,A_i \vdash B_1,\ldots,B_j\] they used a sequent like \[\vdash \lnot A_1,\ldots,\lnot A_i,B_1,\ldots,B_j\]. In classical logic they are equiprovable. I am very grateful they did this, because it gave me a chance to think about this formalization, and decided what I thought about it. I have realized that for MALL it works quite well, but when we add more structure, like the modalities, it can be confusing, and hard to understand.
This brings us to Damiano Mazza’s lecture “Exponentials Attack!” (slides). Since we are in a single-sided formalization of classical linear logic he introduces the why-not exponential – or as I like to call the modality, because exponential conflicts with the terms use in category theory. This modality is denoted \[?A\]. The sequent calculus rules for this connective are as follows:
The point of this modality is to give us the left two rules which are the structural rules for weakening and contraction. The third rule is called promotion, and allows us to inject any formula into the modality, finally, the fourth rule is called dereliction, but this one looks funny. What is this \[!A\]? In classical logic every connective has a dual connective and as it turns out \[\lnot ?A = !\lnot A\]. However, as one student at the school asked, what does it mean? The lecturer simply said, well, its dual to why-not, and this rule relates them.
This is where the single-sided formalization of linear logic can be confusing. Since \[!A\] is dual to \[?A\] the former should also model some structural rules, but the single sided version does not make this explicit. However, the two sided version does. Consider the following rules for the linear modalities in two-sided fashion:
As the rules show, \[!A\] gives us the structural rules on the left, and \[?A\] gives us the structural rules on the right. Categorically, \[!A\] is a comonad and \[?A\] is a monad, in fact, the promotion rules are the units of these structures. I think that the lecture on modalities could have simply flashed these to the audience and it would have helped. Using these modalities we can now encode non-linear classical logic in linear logic.
The final lecture of the school was by Lionel Vaux on denotational semantics (slides). It was very good! I really enjoyed learning about the relational models and the coherence spaces. It was nice to see the semantics related to the proof nets.
The school was quite good, and I liked how consistent everyone was with the content. All the lecturers used the same syntax and knew exactly what the others were going to teach. This made everything a lot easier to follow. I liked a lot the notion of having a school just before a series of conferences or workshops, because it can help prepare new graduate students to better understand the basics before being hit with the conference talks.
Directly following the school was the workshop Linear logic and philosophy. The coolest part of this workshop was that Girard was an invited speaker! Yes, I saw Girard. It was really cool. I am not a philosopher, and so I really cannot comment much on this workshop. Admittedly, I did not stay for the entire workshop, and used the time to take in Lyon. Checkout the photos at the end of this page for some things I saw.
Following the philosophy workshop there was the workshop on Linear logic, mathematics and computer science. This was the whole reason I went, and I was very much looking forward to going. I am new to the linear logic community, and so I was looking forward to getting a chance to connect and meet new people. The workshop did not disappoint!
During the first day I gave a talk called “On Linear Modalities for Exchange, Weakening, and Contraction”; click the image to the left to see the slides. This talk is related to my attack trees project, and it seemed to be well received. I got some good feedback, and a number of people told me they liked my talk. So that’s good. I was very nervous, because there were some big names in the crowed. I also thought that this talk, being about the structural rules to model various computational structures like processes would be kind of an outlier, but how wrong I was. The topic of my talk fit in quite well with other talks, and even suggested new connections. So I take this talk as a success.
There were two recurring topics of this workshop: graphical models of substructural logics like variations of proofs nets, and the concept of graded or bounded linear logic. However, there were two talks on non-commutative linear logic, mine and one on connections to linguistics. There were a few others as well.
Graded/bounded linear logic is quite new, and I think will have connections to my project as well. Dominic Orchard gave a great talk on this. The idea is to replace the usual linear modality \[!A\] – here we will be in intuitionistic linear logic – with the modality \[!_r A\] where \[r \in R\] and \[(R, 0, +, 1, \times)\] is a semiring. The modality \[!A\] says that \[A\] can be used as many times as we wish, but \[!_r A\] not only tells us that \[A\] can be used any number of times, but tells us that it has been used exactly \[r\] times. The operations of the semiring are then used in the inference rules to calculate each \[r\]. Here are a few examples:
I think this may lead to a way to add the costs on attack trees in my project. Check out the list of talks here.
One finally point about the workshop. I was happy to see that it was not an all male event. There were a number of female participants as well as three talks by women. Hopefully, in the future we will have an even split, but this is better than zero.
This workshop was also great for networking. This was the first time I met Dominic Orchard and it seems we have a lot of similar interest. I finally got to meet Paul-André Melliès, and he even taught me some new tricks with composing comonad/monads using adjoints which has me very excited. I greatly admire his work, and he is a super nice guy! All in all, the trip to Lyon was fantastic. Check out some photos: 
