Statement

Logic

The purpose of this symposium is to present works on a new possible way of re-building Logic and re-thinking Language starting from the concept of interaction, in the frame of Ludics, a pre-logical formalism invented by J-Y. Girard. Ludics has appeared in 2001 in the continuation of Girard’s researches on Geometry of Interaction. It is linked, on one side, to the works on focalisation of proofs in linear logic (a discovery made by J-M. Andréoli at the beginning of the nineties) and, on another side, to a deeper approach of the notion of proof-net. As is well known now, the techniques of proof-nets provide a way of objectivizing proofs, simply as geometric devices (graphs) on which criteria (like acyclicity or connectedness) are checked. Following these techniques, proofs revealed to be less based on formulae (and sequent rules) than on locations where connections can be made. Moreover, the provability is shown by completely different means than explicit derivability rules. The first researches which were held on Ludics actually concerned its links with proof-nets.
It has also been possible to establish a relation with coherent spaces, which provide a semantics for linear logic.
Ludics also provides a convenient frame to rebuild a second-order logic (of the F-system kind), while the question of the first-order is still open : to recast these questions in a more interactive frame is a challenge and will be particularly put in light on the question of generalized quantifiers.
Because they are based on a « localist » conception according to which the rules are defined on directories of addresses instead of being defined on formulae, the methods of Ludics allow one to reconstruct formulae and connectives by means of interaction between designs (trees built by using rules), which, in the same movement, gives an interactionnist view on meaning.
K. Terui, by extending a presentation of Ludics by Curien, has proposed a relation with the theory of formal languages : c-designs are computational versions of Girard’s designs which allow one to rebuild all the concepts of the classical computability theory.

Natural language, meaning and Learning

Beyond the theoretical objectives aforementioned, the use of the ludical concepts will be shown, on domains like languages (natural as well as artificial ones, the later being for instance the web languages) and modelling of learning in interactive situations.
This symposium will particularly rest on the results obtained during the PRELUDE project, which was funded by the French National Agency for Research from 2006 to 2009, and on the works presently done in the continuation of this project, the LOCI project, funded by the same agency for the period between 2010 and 2014. These works have concerned theoretical pragmatic (particularly applied to the theory of dialogue) and the semantic of natural language. By completing the approaches known under the name of « proofs as meanings », as they have been proposed by Aarne Ranta, elaborating on Martin-Löf’s Type Theory, they are based on the concept of « design » which is an extension of the concept of proof, including the dual notion of « counter-proof », and allows one to rigorously define a notion of interaction, via a normalisation procedure applied to a net of designs. This notion provides a basis of a possible representation of dialogues (in argumentation theory for instance), as well as a basis for expressing the representational content of utterances from a dialogical perspective, a conception which is developed in the frame of Brandom’s inferentialism.
Speech acts, assertion and negation and the use of quantificational expressions in ordinary language will be addressed.

Artificial languages

Moreover, interaction is the core of web applications. From its very beginning, the installation of the web has facilitated use and distribution of resources across the Internet. Two particular aspects are studied and will be taken into account during the symposium:
From interaction to web languages
Programming languages adapted to the web, as well as software libraries have to integrate the client-server paradigm to be useful in web situations. Previous approaches (even those based on continuations) don’t allow to apprehend the particular dialogues, before making explicit the closure of the dialogues accepted by a program, that is its type. This stage becomes necessary for web services where it is a set of trees of potential exchanges which allows the best to characterize programs. The classical way for dealing with web services, which starts from a language of description of contracts to type the interactions, does not take into account all the procedural situations. It is suggested that interaction be the elementary principle from which programming concepts are redefined.
Ontologies and folksonomies
Semantic Web is the initiative supported by the W3C that aims to make the WorldWideWeb a place of interaction among machines — or at least among their ``representatives’’ known as autonomous agents — thanks to the exchange of ``labelled’’ data. It is clearly something more complex and more interesting than today’s Web, which allows only for the exchange of files and ``raw’’ data that machines simply display on a monitor.
However, while the top-down approach of the Semantic Web initiative looks like being too close to Artificial Intelligence, the bottom-up practices of Web2.0 lack any theoretical set-up to be really useful for autonomous agents’ operations.
The geometric framework of Linear Logic is well suited for that purpose. The web situation may be studied by using Ludics concepts, the aim being not only to model the structure but also the operations.