Notes sur l'article de Rehof-Sørensen sur lambda-delta
------------------------------------------------------
(version initiale de septembre 2007)

C'est le calcul \-F par nom sans variables libres de continuations et
avec F-elim:

(1)   \x.M N                -> M[N/x]
(2)   (Delta x.M) N         -> Delta x.M[\y.x (y N)/x]
(3)   Delta x.x M           -> M                        (si x pas dans M)
(4)   Delta x.x Delta _.x M -> Delta x.x M

F-lift (2) ne diffère de C-lift' (de Felleisen-Hieb) que par l'absence
de A dans la règle de lift (comme chez de Groote).

Le calcul ne peut pas accepter F-idem parce qu'il n'y a pas de
différence entre les variables de termes et les variables de
continuations, et que la règle Delta x.k Delta y.M -> Delta x.M[k/y]
ne fait pas de sens en CBN; c'est le problème standard mentionné par
Hofmann-Streicher 2002 [Ajout de février 2010].

Toujours est-il qu'il y a CR (même preuve que chez Felleisen-Hieb je
suppose) et SR (puisque rien ne parle de la continuation toplevel).

Le grand intérêt de cette approche est sa proximité avec les preuves
de normalisation de la déduction naturelle classique (où tp est
interprété par \x.x).


Note (mai 2011): Je n'ai pas pu trouvé de référence à pseudo-classical
typing dans la thèse de Murthy 1990. Ne serait-ce pas plutôt sa note au
continuation workshop 92 ?