Cut elimination procedures for deep inference calculi such as BV and its extensions have traditionally required intricate reasoning about rewriting proofs into normal form. I will present another way, based on ideas from the rewriting-free Normalisation by Evaluation (NbE) technique for lambda-calculi. NbE works by constructing a model from the syntax of normal (or cut free) proofs and evaluating proofs containing cut into that model. A reification procedure then reads out the normalised (cut free) proof from the interpretation. I will show that this technique works for BV and its extensions with additives and exponential. This is joint work with Wen Kokke.
Period
25 Jul 2026
Event title
Sixth International Workshop on Structures and Deduction 2026