From e9e2585db1b1c45917e80d53b2c372b0e76f7b44 Mon Sep 17 00:00:00 2001 From: Pablo Donato Date: Fri, 25 Mar 2022 16:44:55 +0100 Subject: [PATCH] Ajout d'une section Ludique --- README.md | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/README.md b/README.md index cea97e3..e7052a2 100644 --- a/README.md +++ b/README.md @@ -26,6 +26,34 @@ La partie II explique la construction des flots et la représentation des expone - [“Information, Processes and Games” (section 1 & 5) – Samson Abramsky](https://arxiv.org/abs/1604.02603) - [“Symmetry and interactivity in Programming” – Pierre-Louis Curien](https://hal.archives-ouvertes.fr/hal-00003868/) +## Ludique + +On peut voir la ludique comme une version *alpha* de la syntaxe transcendentale, qui met complètement de côté l'usine pour se concentrer sur l'usage. On arrive déjà à expliquer les additifs, le second ordre, et avec [un peu de travail](https://www.irif.fr/~faggian/pubs/LXfin.pdf) les exponentielles. Mais bien sûr sans parler de critères de correction. + +On pourra s'y intéresser: +1. comme première tentative de conceptualisation technique de l'usage, riche en terminologie et théorèmes; +2. comme point de référence/comparaison en tant que substrat calculatoire fécond pour la logique. + +Introductions techniques: + +- ["Locus Solum" -- Jean-Yves Girard](https://girard.perso.math.cnrs.fr/0.pdf) ~ L'article fondateur. Un must-read pour les amateurs d'excentrisme. +- ["La ludique" -- Thomas Seiller](https://www.seiller.org/documents/ludique.pdf) ~ Une version compréhensive et synthétique de Locus Solum. +- ["Introduction to linear logic and ludics, Part II" -- Pierre-Louis Curien](https://arxiv.org/pdf/cs/0501039.pdf) ~ Très orienté sur la syntaxe, pour les informaticiens. + +Introductions non-techniques: +- ["Ludique : une logique sans axiome d’identité ?" -- Alain Lecomte](https://hal.archives-ouvertes.fr/hal-00422691/PDF/ExposePEPS.pdf) + +Applications à l'informatique: +- ["Computational ludics" -- Kazushige Terui](https://www.irif.fr/~saurin/Enseignement/LMFI/2018-19/presentation-articles/computational_ludics.pdf) ~ Première version moniste de la théorie des langages/automates, avec en vue la théorie de la complexité. +- ["Towards Ludics Programming: Interactive Proof Search" -- Alexis Saurin](http://www.lix.polytechnique.fr/Labo/Alexis.Saurin/Recherche/Publi/saurin_iclp08.pdf) ~ Comprendre le statut logique des opérateurs de recherche de preuve en programmation logique, style `cut` (pourrait s'étendre aux langages de tactiques dans les assistants de preuve). +- ["On the infinitary proof theory of logics with fixed points" -- Amina Doumane](https://perso.ens-lyon.fr/amina.doumane/these.pdf) ~ Induction, co-induction, model-checking +- ["Ludics and Web: Another Reading of Standard Operations" -- Christophe Fouqueré](https://link.springer.com/chapter/10.1007/978-3-642-19211-1_4) ~ Systèmes de types pour l'interaction sur le web + +Applications à la linguistique: + +- ["Une introduction à la Ludique et à ses applications à la Pragmatique" -- Alain Lecomte, Myriam Quatrini, Marie-Renée Fleury-Donnadieu](https://halshs.archives-ouvertes.fr/halshs-00122747/document) +- ["Dialogues in Ludics -- Marie-Renée Fleury, Myriam Quatrini, Samuel Tronçon"](https://www.researchgate.net/profile/Samuel-Troncon/publication/221350114_Dialogues_in_Ludics/links/00b7d52b2abfeee70b000000/Dialogues-in-Ludics.pdf) + ## Anti realisme - [“Radical anti-realism and substructural logics” – Jacques Dubucs & Mathieu Marion](https://halshs.archives-ouvertes.fr/halshs-00000055/)