Invited talk
Title: Focusing, computation, specification and reasoning
Elaine Pimentel (Universidade Federal do Rio Grande do Norte)
Abstract:
Focusing for linear logic in the 1990’s opened a new and exciting research directions in proof theory. In fact, determining different levels of non-determinism in logical systems not only improves proof search procedures in such logics, but also allows the use of logic in many applications not imagined before. In this talk, we will show some of such applications.
We start by showing how focusing allows for determining (correct) optimization procedures for concurrent programs. More specifically, we show that it is possible to give a logical characterization to concurrent constraint programming (CCP) with the highest level of adequacy. This allows the use of logical machinery for reasoning about the behavior of programs. We also show how to characterize maximal-parallelism semantics for CCP by relying on a multi-focusing discipline for intuitionistic linear logic (ILL).
This mechanism of adequately translating systems into linear logic can also be applied to a number of logical systems, making linear logic a suitable framework to reason about such systems. Surprisingly, this translation can also be used in order to automatically generate focused versions of the specified systems. We will present a case study in this direction.
Focusing discipline plays an important role also in other logics. For example, Miller and Liang proposed LJF, a focused proof system for intuitionistic logic that allows for atoms of different polarities. We show how to use maximal multi-focusing in order to identify proofs in LJF, obtaining a 1-1 translation between maximal proofs in LJF and proofs in the natural deduction system for intuitionistic logic (NJ). We hence move toward solving the problem of identity of proofs in intuitionistic logic in the sequent calculus setting.
Finally, we will show advances in the quest of proposing focusing for other proof systems, not necessarily sequent-calculus based. More precisely, we propose a notion of focusing for nested sequent calculi for modal logics which brings down the complexity of proof search to that of the corresponding sequent calculi.