Thrusday 12 January 2023, 14:00, room 3U47 and online: Intersection Types in Deduction Modulo Theory, Olivier Hermant (CRI, Mines Paris, PSL University), joint work with Ronan Saillard.

In a 2012 paper, Richard Statman exhibited an inference system, based on second order monadic logic and non-terminating rewrite rules, that exactly types all strongly normalizable lambda-terms. We show that this system can be simplified to first-order minimal logic with rewrite rules, along the Deduction Modulo Theory lines.

We show that our rewrite system is terminating and that the conversion rule respects weak versions of invertibility of the arrow and of quantifiers. This requires additional care, in particular in the treatment of the latter. Then we study proof reduction, and show that every typable proof term is strongly normalizable and vice-versa.