Operational Modal Logic
by Sergei Artemov
This work is closely related to our previous study of reflection in type theory. The modal logic he has in mind is Godel's system S4, a logic of provability. Sergei has a new axiomatization which uses "proof expressions" and is related to propositions-as-types. He shows the logic complete in two senses which he will explain.