Weak normalization of the Lambda mu calculus with the rules mu' and rho


Peter Battyanyi, . 5 janvier 2006 10:15 limd 2:00:00
Abstract:

Le lambda mu calcul symétrique (i.e. le calcul où on a ajouté la règle mu' duale de mu) est fortement normalisable dans le cas typé. Pourtant quand on ajoute la règle rho qui semble n'être qu'une règle de simplification, la forte normalisation est perdue. On garde cependant la faible normalisation. C'est ce qu'on montrera dans cet exposé.