Nous adaptons le kit syntaxique de Curien-Herbelin afin de donner un
compte-rendu syntaxique précis des preuves focalisées (en calcul des
séquents) de la logique linéaire.  L'exposé analyse divers choix
syntaxiques, que l'on regroupe de manière générique (en suivant Munch)
sous le nom de "système L".

L'exposé comprend cinq parties:

1) rappel du kit syntaxique:   "lambda bar", "mu", "mu tilde". Le  
slogan principal est qu'une coupure correspond (Curry-Howard) à un  
état d'une machine abstraite.

2) Le cadre polarisé / focalisé.  Ici le slogan est "rompre la  
symétrie complète gauche-droite (ou positif-négatif) pour obtenir  
la confluence dans un cadre classique".

3) Première syntaxe (Curien): introduction d'une notion de  "contre- 
motif" qui colle particulièrement bien à la décomposition  
réversible des connecteurs à gauche (ou négatifs) (cf. aussi les  
éliminations gauches dans les tactiques Coq).  Cette syntaxe  
souligne que "bénitier (Andreoli-Girard) = valeur (Plotkin)".

3.5) Critique de cette syntaxe, qui réalise un quotient bancal sur  
les preuves.

4) Deuxième syntaxe (Curien): on quotiente davantage et on arrive  
au "système L synthétique", qui ressemble à la logique LU de  
Zeilberger et à la ludique. Le grain de sel original ici est un jeu  
entre  motifs et contre-motifs.

5) Les syntaxes suivantes sont inspirées par le travail de Munch  
(http://perso.ens-lyon.fr/guillaume.munch ):

a) On considère les contre-motifs comme du sucre syntaxique (et au  
passage on quotiente moins);

b) On distingue la dualité droite/gauche (code/environnement) de la  
dualité positif-négatif (eager/lazy), de façon à pouvoir distinguer  
un tenseur strict d'une somme lazy.  De plus, on permet le mélange  
strict/lazy grâce à des opérateurs "shift" de changement de polarité.

c) On passe à une syntaxe "faiblement polarisée" où la polarité  
d'une formule est  seulement donnée par celle du connecteur de  
tête. Ceci permet de garder les shifts implicites. On aboutit ainsi  
au "système L focalisé (bilatéral)" de Munch (dans une variante  
avec bénitier).