Task 6: Formal questions around ludics
Ludics, coherent spaces and first order
Work in the PRELUDE project raised formal issues incompletely or not at all considered a til now that
we should now deal with. The basic objects of Ludics are chronicles which satisfy certain properties,
the design being a coherent subset and a behaviour a set of designs closed by orthogonality.
- ludics, c-designs : c-designs generalize Ludics’ designs.
We propose to address the issue of the fragments generated by tree languages whose complexity
analysis, generation, learning is polynomial, like what has been done within the lambda-calculus (cf.
S. Salvati, 2009)
- behaviours in Ludics : the concept of incarnation was introduced by J.-Y. Girard to characterize the
subset of designs in a behaviour which minimally defines it. How to characterize such behaviour more
precisely, the intrinsic relationship between incarnation and behaviour, the relationship with the
coherent spaces? - ludics and first-order : the link between Ludics and first order is to deepen after the work of
Fleury and Quatrini. We will in particular consider the case of attribute value structures without
terms, the link between quantification and connectors "with" indexed, and finally the "braiding"
categorical model with first order.
Formal questions around Ludics
Coordinator : Christian Retoré (SIGNES)
Members : Christophe Fouqueré (LIPN), Myriam Quatrini (IML), Marie-Renée Fleury (IML),
Sylvain Salvati (LaBRI), Lionel Vaux, Thomas Seiller (IML)
External collaborators : Paul-André Melliès PPS – Paris 7), François Lamarche (LORIA)
Objectives :
Study of properties of Ludics related to C-designs, the concept of incarnation, first order
Content :
- ludics, c-designs : (LABRI) study of fragments that can be generated by tree languages
whose complexity analysis, generation, learning is polynomial - behaviours in Ludics : (LIPN, IML) minimal characterization of incarnation, links with
coherent spaces - Ludics and first order : (SIGNES, LIPN, IML) : Study of attribute value structures without
terms, the link between quantification and indexed connectors "with", "braiding" of categorical
model with first order.
