Elaine wanted to discuss some more mathematical ideas that she might (or not) want to talk to her students about. Sitting in the several planes that it took me to get home, I made a preliminary list of things that I wanted to talk to her about.#1. Dialectica categories relationship to Milner's "tacticals", in Budiu et al's partial compilers paper. Also relationship to sub-exponentials, as Dialectica categories have three notions of modalities.
#2. Hopf (co)-algebras in Dialectica categories (Blute/Majid?).
#3. Prove (using TATU perhaps?) cut-elimination for FILL. I guess this is hard, given what she said about multiple-conclusion versions of IL.
#4. Proof-theoretical institutions. Why my work with Rabe et al is not good enough. as far as I'm concerned, that is.
:) Good to have lots of things to think like that :) I will start right away. Some more at the end of this week.
ReplyDeleteOba!!! Will carry on adding references and reading the papers you've mentioned, as soon as I can.
Delete