The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
The most flexible strong normalization proofs methods for various extensions of typed lambda-calculi use type interpretations. Among them we distinguish Girard's reducibility candidates, Tait's saturated sets and interpretations based on biorthogonality. In this talk we compare these different interpretations wrt their ability to handle rewriting and wrt their stability by union.
We first propose a generalization of the notion of neutral term in Girard's
candidates that allows to define them in a generic way. Concerning stability by union, we recall that there are confluent typed rewrite systems that do not admit stable by union type interpretations. We present a necessary and sufficient condition for Girard's candidate to be stable by union and a necessary and sufficient condition for the closure by union of biorthogonals to be reduciblity candidates. The second condition is strictly more general than the first one, and allows to define Tait's saturated sets for rewriting in a uniform way. Moreover, we show that for orthogonal constructor rewriting, Girard's candidates are stable by union.