LSV Seminar

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.

Past Seminars

Unions of Type Interpretations

Visit website for this news | Export event in iCalendar format

Date
Tuesday, January 29 2008 at 11:00AM
Place
Salle de Conférence (Pavillon des Jardins)
Speaker
Colin Riba (INRIA Sophia Antipolis)

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.


About LSV

Agenda

Export agenda in iCalendar format | Past seminars

Tue, Jan 22
Tue, Jan 29
Tue, Feb 5
Tue, Feb 19

Past seminars