Théorie des types et réalisabilité
Mercredi 8 décembre 2021, 14 heures, Salle 1007
Federico Olimpieri (Université de Leeds) Categorifying Intersection Types
Théorie des types et réalisabilité
Mercredi 24 février 2021, 14 heures, online (https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7)
Elaine Pimentel (UFRN - Brazil) On linear logic, modalities and frameworks
We then move to the question of giving an interpretation to subexponentials. We will show a game interpretation of affine linear logic with subexponentials, viewing the game as a playground for illuminating semantic intuitions underlying resource conscious reasoning. Interestingly enough, this led to the proposal of new sequent systems for capturing the notions of costs and budget in a fragment of linear logic with subexponentials, thus opening new possibilities for analysing the problem of comparing proofs.
We finish the talk by showing a computational interpretation of subexponentials in the process-as-formula fashion, where process constructors are mapped to logical connectives and computational steps are related to proof steps. In particular, we will show in detail the role of pre-orders in subexponentials for the adequate specification of different modalities in concurrent systems, such as time, space, epistemic and preferences. We end with a discussion about which new models of computation should arise from the extension of the concept of modality in linear logic.