seminaire PPS Jeudi 2/7

Chers tous,
le prochaine seminaire PPS est

le Jeudi 2 Juillet,
11h, salle 0C2:

Naohiko Hoshino (RIMS, Kyoto)

Title
Linearization of realizability

Abstract
For every PCA (partial combinatory algebra), we can construct
categories such as effective toposes, assemblies and PERs
(partial equivalence relations). They provide models of
polymorphic lambda calculus and dependent type theory.
In this talk, we consider linearlization of constructions
of these categories. Instead of PCA, we consider an algebra
that is a slight generalization of Abramsky's linear combinatory
algebra (LCA) and observe that construction of assembiles
and PER works well. On the other hand, it appears that
the linearization of the construction of an effective topos
from a tripos, called the Set(p) construction, does not work.

seminaire PPS Jeudi 25/6

Chers tous,
le prochaine seminaire PPS est

Jeudi 25 Juin, 11h, salle 0C2:

Colin Riba (ENS Lyon)

On the Values of Reducibility Candidates

Abstract:
The straightforward elimination of union types is known to break
subject reduction, and for some extensions of the lambda-calculus, to
break strong normalization as well. Similarly, the straightforward
elimination of implicit existential types breaks subject reduction.

We propose elimination rules for union types and implicit existential
quantification which use a form call-by-value issued from Girard's
reducibility candidates. We show that these rules remedy the above
mentioned difficulties,
for strong normalization and, for the existential quantification, for
subject reduction as well.

seminaire PPS Jeudi 11/6

Chers tous,
le prochaine seminaire PPS est

Jeudi 11 Juin,
11h, salle 0C2:

Lorenzo Tortora de Falco (Roma)
Sémantique relationnelle et temps d'exécution en Logique Linéaire

Qu'est-ce qu'un calcul correct ? Une tentative de répondre à la question
est de donner un maximum de place aux calculs non corrects. On sera alors
amené à identifier des propriétés cruciales du calcul, qui seront les
témoins de sa correction (terminaison faible ou forte, confluence,
exécution en temps borné, etc...). En guise d'introduction, je discuterai
du point de vue de la logique linéaire (LL) sur la question, pour prendre
ensuite celui de la sémantique relationnelle sur lequel portera
l'essentiel de l'exposé. Je présenterai les résultats principaux d'un
travail en collaboration avec Daniel De Carvalho et Michele Pagani: 1) un
réseau de preuve de LL est normalisable ssi son interprétation
``exhaustive'' est non vide 2) à partir de l'interprétation de deux
réseaux sans coupures de LL on peut calculer le nombre exact d'étapes
d'élimination des coupures conduisant du réseau obtenu en coupant entre
eux les deux réseaux de départ et sa forme normale. Si le temps le permet,
je discuterai d'une possible amélioration de ce dernier résultat (travail
en cours avec Daniel De Carvalho).