Skip to Main content Skip to Navigation
Theses

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

https://tel.archives-ouvertes.fr/tel-02988166
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

File

edgalilee_th_2017_pavaux.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-02988166, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

56

Files downloads

13