~~NOCACHE~~
/* DO NOT EDIT THIS FILE             */

[[seminaires:types:index|Théorie des types et réalisabilité]]\\
Mercredi 8 décembre 2021, 14 heures, Salle 1007\\
**Federico Olimpieri** (Université de Leeds) //Categorifying Intersection Types//
<button type="link" size="xs" collapse="b17-3364">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b17-3364" collapsed="true">
<well size="sm">
We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.
</well>
</collapse>


[[seminaires:types:index|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//
<button type="link" size="xs" collapse="b17-3365">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b17-3365" collapsed="true">
<well size="sm">
We start by presenting a local system for linear logic (LL) based on linear
nested sequents. Relying on that system, we propose a general framework for
modularly describing systems combining, coherently, substructural behaviors
inherited from LL with simply dependent multimodalities. This class of
systems includes linear, elementary, affine, bounded and subexponential
linear logics and extensions of multiplicative additive linear logic (MALL)
with normal modalities, as well as general combinations of them.

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.
</well>
</collapse>