The other talk was Christoph Benzmüller selling us on his higher-order theorem prover Leo II, which sounds pretty awesome. It pulls a bunch of tricks to reduce theorem proving problems in HOL to bits and pieces it feeds to first-order provers, and then digests the results, and then feeds back into the first-order provers, and so on. I have a meeting with him and Frank tomorrow morning to see if I can get it to do linear logic proving by pulling the same encoding tricks I did with HLF. It sounds like he already got some cool results with Deepak's authorization logic already.
I've found myself thinking recently about something
neelk mentioned, which is that we lambda-calculus people really ought to "already" understand something of the 2-categorical structure of adjunctions (for example between - x A and A ⇒ -) because we know that you should privilege β-reduction and η-expansion, this being a finer-grained notion than just adjunction, which says by dint of uniqueness of adjoint transposes that you just get equality of terms that are connected βη-convertibility in any direction and indeed any zigzagging path you like.Poking at the literature a bit, it seems the right word to look for is "biadjoint" (or occasionally "pseudoadjoint"?) but it seems that if you are smart enough to confidently talk about what biadjoints are in a published paper, you are smart enough to make everything else in your paper impenetrably advanced, so I haven't made a lot of progress understanding them.
---
ETA: But I did make this model in Sketchup, which I think is the analogue of the adjoint triangle equalities one dimension up:
