"Focusing with higher-order rules"
What makes Andreoli's notion of focusing proofs so robust? In this
talk, I will try to argue for the naturality of focusing by giving a
new presentation that makes very explicit the duality between focus
and inversion, and between positive and negative polarity. Loosely
inspired by Girard's ludics, the idea is to stratify the definition of
a focusing sequent calculus into two stages: first define a form of
"pattern-typing", and then define the focusing judgments by
quantifying over patterns. Focus quantifies existentially, while
inversion quantifies universally---positive connectives quantify over
constructor patterns, negative connectives over destructor patterns.
Besides giving a simple account of evaluation order and
pattern-matching, this style of presentation has the benefit of being
amenable to modular extension, since we potentially can encode many
features into pattern-typing without affecting the overall structure
of focusing proofs, or the meta-proofs of identity and cut. I will
describe a few of these extensions, which are still preliminary --
audience feedback appreciated!