Multi-Focusing on Extensional Rewriting with Sums
Gabriel Scherer · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2015
We propose a logical justification for the rewriting-based equivalence procedure for simply-typed lambda-terms with sums of Lindley. It relies on maximally multi-focused proofs, a notion of canonical derivations introduced for linear logic. Lindley’s rewriting closely corresponds to preemptive rewriting, a technical device used in the meta-theory of maximal multi-focus.