Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Unions of Type Interpretations

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

Date
Le mardi 29 janvier 2008 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
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.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents