Types in Ludics
Eugenia Sironi
I2M, Aix-Marseille Université
Date(s) : 15/01/2015 iCal
14h00 - 16h00
This thesis proposes a representation of the notion of type, with a particular interest on dependent types, in Ludics.
Ludics is a theory introduced by Girard. It comes from a fine analysis of the multiplicative, additive fragment of polarized Linear Logic (MALL_p). One of its aim is to reconstruct logic from the notion of interaction.
A type is a class of objects that behave in the same way with respect to other objects.
The notion of type is common to several domains as Computation Theory, Game Semantics and Martin-Lof’s Intuitionistic Type Theory.
Using the terminology of Martin-Lof, the canonical terms of a type are the primitive elements of the type, that is the objects that characterize it. The non-canonical terms are the terms obtained by applying some operations on canonical terms and that once computed give a canonical term. Terms are seen as programs and two terms are equal when their computation gives the same result, that is the same canonical term.
We introduce the notion of principal behaviour, that is well-suited to represent canonical terms. We introduce also the notion of separable behaviour, that gives us a tool to define functions in a simple way.
We represent natural numbers, lists, records, dependent functions, pairs and discuss dependent record types.
We focus then on Martin-Lof’s Type Theory and propose the first steps to represent some basic types and constructions.
*Membres du jury :
–
– Vito Michele Abrusci.
– Claudia Faggian (PPS, Paris 7).
– Christophe Fouquéré (LIPN, Paris 13), codirecteur.
– Myriam Quatrini (I2M, Marseille), codirectrice.
– Laurent Regnier (I2M, Marseille).
– Christian Retoré (LIRMM, Montpellier), rapporteur.
Liens :
– https://ca.linkedin.com/in/eugenia-sironi-7341a6b8/fr?trk=people-guest_people_search-card
– theses.fr
Catégories
