Focusing Rules!

Me and Dale finished the last week a new paper, which we already submitted to IJCAR: Focusing in Linear Meta Logic. The paper shows that by changing focusing annotations in a same meta-logic specification one can encode different object-logics. There are several interesting observations and results in the paper: First, the specification we use is very declarative; for instance, object-logic rules do not contain side formulas. Second, we obtain adequacy results for several proof systems, from sequent calculus to natural deduction and tableaux systems. Third, from these adequacy results, one can interpret that these different systems are, in fact, just systems with different focusing annotations. Fourth, from these adequacy results and linear logic's focusing and cut-elimination theorems, we obtain new modular soundness and (relative) completeness results for all these systems.

We will only know if the paper is accepted in April. Hope the reviewers enjoy focusing as much as I do!