Author: Olivier Hermant
Title: Semantical Cut Elimination in Intuitionistic Deduction Modulo
Abstract: 
In this talk, we will show techniques that allows to show cut
elimination for a wide range of rewrite systems in deduction
modulo. The frame is Intuitionnistic Sequent Calculus Modulo, and we
show soundness and completeness of the cut-free calculus w.r.t. Kripke
Structures, one of the well-known semantics of intuitionnistic
calculi. We show these results for some wide conditions on the rewrite
system, and at last exhibit a system ehancing cut redundancy, although
non-normalizing.