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
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: