Skip to Main content Skip to Navigation

Inductive, Functional and Non-Linear Types in Ludics

Abstract : This thesis investigates the types of ludics. Within the context of the Curry–Howard correspondence,l udics is a framework in which the dynamic aspects of both logic and programming can be studied. The basic objects, called designs, are untyped infinitary proofs that can also beseen as strategies from the perspective of game semantics, and a type or behaviour is a set of designs well-behaved with respect to interaction. We are interested in observing the interactive properties of behaviours. Our attention is particularly focused on behaviours representing the types of data and functions, and on non-linear behaviours which allow the duplication of objects. A new internal completeness result for infinite unions unveils the structure of inductive data types. Thanks to an analysis of the visitable paths, i.e., the possible execution traces, we prove that inductive and functional behaviours are regular, paving the way for a characterisation of MALL in ludics. We also show that a functional behaviour is pure, a property ensuring the safety of typing, if and only if it is not a type of functions taking functions as argument. Finally,we set the bases for a precise study of non-linearity in ludics by recovering a form of internal completeness and discussing the visitable paths.
Complete list of metadatas

Cited literature [58 references]  Display  Hide  Download
Contributor : Abes Star :  Contact
Submitted on : Wednesday, November 4, 2020 - 3:13:48 PM
Last modification on : Friday, November 6, 2020 - 4:56:18 AM


Version validated by the jury (STAR)


  • HAL Id : tel-02988166, version 1



Alice Pavaux. Inductive, Functional and Non-Linear Types in Ludics. Computer Science and Game Theory [cs.GT]. Université Sorbonne Paris Cité, 2017. English. ⟨NNT : 2017USPCD092⟩. ⟨tel-02988166⟩



Record views


Files downloads