Wiki de logique linéaire
Pour tout(e) question / ajout / correction : m'envoyer un mail (olivier.laurent@ens-lyon.fr).
Installation
Wiki
La machine llwiki.ens-lyon.fr (fournie par le LIP et installée en DMZ à l'ENS Lyon) fait tourner un moteur MediaWiki (celui utilisé pour Wikipedia) avec :
- une distribution LaTeX tex-live
- quelques paquets LaTeX complémentaires : cmll, bussproofs, llwiki
- un texvc modifié notamment pour utiliser le paquet llwiki (développement sur lipforge)
N'importe qui peut se créer un compte sur le wiki, mais la modification des pages est restreinte aux personnes dont le compte a été validé par un administrateur (bureaucrat).
Listes de diffusion
Serveur de listes
LaTeX
Les développements logiciels en cours sont accessibles sur lipforge.
- syntaxe hyper-contrainte "microtex" avec outils de passage a wikitext
- fichier externe de macros géré par une personne
- méthode canonique haut niveau de saisie pour :
- des preuves de calcul des séquents : syntaxe en polonaise inversée (notation postfixe), première implémentation par bussproofs
- des réseaux ???
- des diagrammes catégoriques : xymatrix, tikz
- ...
Premier plan
Les pages suivantes semblent nécessaires pour démarrer. Des pages très naturelles (ludique, logique linéaire différentielle, ...) sont volontairement omises : elles devraient se créer naturellement par le mécanisme wiki (quelqu'un de motivé s'y mettra et démarrera la page).
- Logique linéaire (style baratin)
[L.Regnier]
- Calcul des séquents
[E.Beffara]
- Fragments
[D.Mazza]
- Logique linéaire intuitionniste
[O.Laurent]
- Réseaux de preuve
[suspendu !!!]
- Sémantique
- catégorique
[S.Mimram]
- des phases
[T.Ehrhard]
- cohérente
[L.Regnier|T.Ehrhard]
- relationnelle
[T.Ehrhard]
- GoI
[L.Regnier]
- jeux
[P.Clairambault]
- Traductions classiques et intuitionnistes
[O.Laurent]
- Systèmes à complexité bornée
[P.Baillot]
Les responsables indiqués ci-dessus s'engagent à assurer le démarrage rapide de la rédaction d'un contenu substantiel dans les pages correspondantes.
- ne pas s'embéter avec ça au tout début
- création d'une association à laquelle céder les droits ?
- les auteurs cèdent tous leurs droits ?
- le contenu du wiki est rendu utilisable sous licence cc by nc sa ?
Règles d'usage
- vrais noms pas pseudos
- tout en anglais même les discussions
- respect des macros LaTeX
- acceptation de la licence ?
Questions soulevées
- Une liste de choses à faire dans le wiki
- Mise en place d'un comité d'arbitrage ?
- Mise en place d'un comité technique ? à l'intérieur du comité de rédaction ?
- Droits / licence (voir plus haut) ?
- Comment traiter les réseaux de preuve ? (nécessitera certainement une réunion dédiée)
- Achat d'un nom de domaine ? par qui ?
- Aura-t-on besoin de financement ?
- Macros pour les systèmes logiques : LL, MLL, MALL, ... ?
- Meilleure mise en valeur des définitions, théorèmes, ... : texte en italique ?
- Emmanuel Beffara (IML)
- Pierre Boudes (LIPN)
- Thomas Ehrhard (PPS)
- Jean-Yves Girard (IML)
- Olivier Laurent (LIP)
- Laurent Regnier (IML)
- Lorenzo Tortora de Falco (Roma 3)
- Patrick Baillot (LIP)
- Emmanuel Beffara (IML)
- Pierre Boudes (LIPN)
- Pierre Clairambault (PPS)
- Marc de Falco (IML)
- Thomas Ehrhard (PPS)
- Jean-Yves Girard (IML)
- Florian Hatat (LAMA)
- Tom Hirschowitz (LAMA)
- Pierre Hyvernat (LAMA)
- Olivier Laurent (LIP)
- Damiano Mazza (LIPN)
- Samuel Mimram (PPS)
- Michele Pagani (Turin)
- Aurélien Pardon (LIP)
- Laurent Regnier (IML)
- Alexis Saurin (Turin)
- Christine Tasson (PPS)
- Lorenzo Tortora de Falco (Roma 3)
- Paolo Tranquilli (PPS - Roma 3)
- Lionel Vaux (LAMA)