Deciding equivalence with sums and the empty type

Gabriel Scherer

The logical technique of focusing can be applied to the $\lambda$-calculus; in a simple type system with atomic types and negative type formers (functions, products, the unit type), its…