Towards linear logic: a theory of substructural demonstration, beyond classical and intuitionistic logics

Towards linear logic: a theory of substructural demonstration, beyond classical and intuitionistic logics - THEODEM

Illogical geometry © CDD20 | Unsplash
Status
[in progress] 2021-2023
Type
Junior Laboratory
Situation
Ongoing

Subject

The aim is to offer students from all walks of life an introduction to the theory of demonstration and its associated research topics - without the need for prior knowledge. More precisely, it is a matter of setting up a route from first-order logic to linear logic; in doing so, the following elements will be addressed: theory of models, categories, types, lambda-calculus, linear logic. The exposition of linear logic, which requires knowledge of the other theories, will constitute the goal and the end of this logical itinerary.

Creation Date

08/11/2021 

Closure Date

30/05/2023

Project Leader

Hugo CADIÈRE, Quentin LE HOUÉROU, Rémi BARRITAULT, Théophile RICHARD DE CAPELE D'HAUPOUL, Roman ALLANIC-PEREZ