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

[[en:seminaires:semantique:index|Semantics]]\\
Wednesday December 20, 2023, 10:45AM, Turing conference room of the Sophie Germain building (first basement) of Université Paris Cité\\
**Paige North** (Utrecht University) //Fuzzy type theory//
<button type="link" size="xs" collapse="b15-3241">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3241" collapsed="true">
<well size="sm">
In this talk, I will report on progress developing a fuzzy type theory, a project that started as part of the ACT 2022 Adjoint School. The motivation is to develop a logic which can model opinions, and we do this by generalizing Martin-Löf type theory. Martin-Löf type theory provides a system in which one can construct a proof (aka a term) of a proposition (aka a type), and we usually interpret such a term as saying that the proposition holds. Fuzzy type theory is a similar system in which one can provide or construct evidence (aka a fuzzy term) to support an opinion (aka a type), but the evidence (fuzzy term) comes with a parameter, for instance a real number between 0 and 1, which expresses to what extent the opinion holds. Martin-Löf type theory is closely related to category theory: from such a type system one can construct a category in which (very roughly) the types become objects and the terms become morphisms, and this can be made part of an equivalence. Thus, we base our development of fuzzy type theory to be the thing which corresponds to categories enriched in a category of fuzzy sets in the same way that Martin-Löf type theory corresponds to categories (enriched in sets).

This is joint work with Shreya Arya, Greta Coraglia, Sean O’Connor, Ana Tenório, and Hans Riess.
</well>
</collapse>
https://paigenorth.github.io/

[[en:seminaires:semantique:index|Semantics]]\\
Wednesday December 20, 2023, 9:30AM, Turing conference room of the Sophie Germain building (first basement) of Université Paris Cité\\
**Réunion De L'Anr Pps**  //Day 2 of the meeting//
<button type="link" size="xs" collapse="b15-3242">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3242" collapsed="true">
<well size="sm">
9:30 - 10:20 Ugo Dal Lago, Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories
10:20 - 10:40 Coffee break
10:45 Semantics working group or (= & of LL) free discussion
</well>
</collapse>
Vous trouverez toute information utile sur la page de l'ANR PPS: https://www.irif.fr/pps-meeting5-2023

[[en:seminaires:semantique:index|Semantics]]\\
Tuesday December 19, 2023, 6PM, Salle 3052\\
**Jacques Sakarovitch** (Telecom Paris) //Conjugacy and equivalence of weighted automata//
<button type="link" size="xs" collapse="b15-3243">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3243" collapsed="true">
<well size="sm">
This talk starts with a result in classical Finite Automata Theory:
'Two regular languages with the same number of words for each length can
be mapped one onto the other by a letter-to-letter (finite) transducer'.

The notion of generating function of regular languages leads to the
introduction of the model of weighted automata.  The conjugacy of
weighted automata, a concept borrowed to symbolic dynamics, is then
defined and it is shown how the above statement can be derived from the
central result of this work: 'Two equivalent weighted automata are
conjugate to a third onewhen the weight semiring is B, N, Z, or any Euclidean domain (and thus any (skew) field)'.

This talk is based on a joint work with Marie-Pierre Béal and Sylvain Lombardy.
</well>
</collapse>
Attention à l'horaire inhabituel

[[en:seminaires:semantique:index|Semantics]]\\
Tuesday December 19, 2023, 10AM, Turing conference room of the Sophie Germain building (first basement) of Université Paris Cité\\
**Réunion De L'Anr Pps**  //Day 1 of the meeting//
<button type="link" size="xs" collapse="b15-3244">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3244" collapsed="true">
<well size="sm">
10:00 - 10:50 Claudia Faggian, Higher Order Bayesian Networks, Exactly
10:50 - 11:10 Coffee break
11:10 - 12:00 Fredrik Dahlqvist, Sampling semantics for probabilistic programs
12:00 - 14:00 Lunch break
14:00 - 14:50 Pedro Azevedo de Amorim, Compositional Expected Cost Semantics for Functional Probabilistic Programs
14:50 - 15:40 Paul-André Melliès, Asynchronous template games and strategies
15:40 - 16:00 Coffee break
16:00 - 16:50 Guillaume Baudart, Schedule Agnostic Semantics for Reactive Probabilistic Programming
16:50 - 17:40 Thomas Ehrhard, A syntax for coherent differentiation
</well>
</collapse>
Vous trouverez toute information utile sur la page de l'ANR PPS: https://www.irif.fr/pps-meeting5-2023

[[en:seminaires:semantique:index|Semantics]]\\
Wednesday November 22, 2023, 10:45AM, Salle 3052, 3ème étage du bâtiment Sophie Germain\\
**Jérémy Ledent** (IRIF) //Simplicial Complex models for Distributed Computing//
<button type="link" size="xs" collapse="b15-3245">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3245" collapsed="true">
<well size="sm">
This will be an introductory talk about geometric methods in fault-tolerant distributed computing. More specifically, my main goal will be to state, and give a proof sketch, of the Asynchronous Computability Theorem of Herlihy and Shavit (1993). This theorem shows that a computational question (can a given protocol solve a distributed task?) can be reduced to a geometric question ("is there a simplicial map between some simplicial complexes?"). This approach has been particularly successful to establish impossibility results in distributed computing. While the original theorem of Herlihy and Shavit was formulated in the specific setting of wait-free processes communicating via shared read/write registers, it it in fact applicable to a much wider class of computational models, and I will try to convey that generality.
</well>
</collapse>


[[en:seminaires:semantique:index|Semantics]]\\
Wednesday November 15, 2023, 10:45AM, Salle 3052\\
**Davide Quadrellaro** (University of Helsinki) //Towards AECats for Team Semantics//
<button type="link" size="xs" collapse="b15-3246">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3246" collapsed="true">
<well size="sm">
Team Semantics generalizes the usual Tarski semantics for first-order logic by interpreting formulas via sets of assignments rather than single assignments. This results in several extensions of first-order logic, such as dependence, inclusion, and independence logic, whose expressive power corresponds to different fragments of existential second order logic. In this talk I will describe how, despite this high expressive power, these logics lend themselves quite well to a model-theoretic investigation. In particular, I will introduce a category of models and higher-order maps for structures in team semantics, and I will try to relate it to the framework of AECats (accessible categories with monomorphisms and suitable colimits) introduced by Kirby.
</well>
</collapse>


[[en:seminaires:semantique:index|Semantics]]\\
Tuesday November 14, 2023, 9:45AM, Salle 1007\\
**Rémy Cerda** (Université d'Aix-Marseille) //Uniformity and the Taylor expansion of infinitary λ-terms//
<button type="link" size="xs" collapse="b15-3247">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3247" collapsed="true">
<well size="sm">
Ehrhard and Regnier's Taylor expansion provides an approximation of λ-terms by vectors of multilinear « resource » λ-terms, and it commutes with normalisation towards Böhm trees. This can be seen as a consequence of the simulation property enjoyed by the extension of the Taylor approximation to the 001-infinitary λ-calculus, as shown in [C. and Vaux Auclair, to appear]. The published version of this extension is only qualitative (the coefficients of the vectors are booleans), but ongoing resarch suggests a quantitative counterpart by reformulating Ehrahrd and Regnier's uniformity arguments. This advocates for considering the 001-infinitary λ-calculus as a "natural" setting for defining th Taylor approximation; a limitation to this statement is that a conservativity property is lost when going infinitary. In addition, adapting our work to 101-infinitary λ-terms suggests a resource λ-calculus approximating the lazy λ-calculus.
</well>
</collapse>
Séance à l'horaire exceptionnel de 9h45 à 11h

[[en:seminaires:semantique:index|Semantics]]\\
Tuesday November 7, 2023, 10:45AM, Salle 3052, 3ème étage du bâtiment Sophie Germain\\
**Masahiro Hamano** (NCKU, Taiwan) //A Measure-Theoretical Linear Exponential Comonad and its Double Glueing Lifting//
<button type="link" size="xs" collapse="b15-3248">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3248" collapsed="true">
<well size="sm">
This talk concerns a category-theoretical construction of linear exponential comonad in terms of measure theoretical transition kernels. 
  (i) A monoidai category of s-finite transition kernels is introduced and shown to have a linear exponential comonad. The s-finitness, recently rediscovered by Staton for probabilistic programming semantics, is a relaxation of the traditional sigma finiteness, allowing the retention of Fubini-Tonelli Theorem, which theorem guarantees the functorial monodical product. Our focus on s-finiteness lies in its ability to accommodate an exponential construction tailored in stochastic process. To achieve this, we employ Melliès-Tabareau-Tasson free exponential construction, utilising equalisers on monoidal symmetries and their limit, These equalisers and limit find instances in measure-theoretic exponential both on measurable spaces and on kernels.
  (ii) A continuous orthogonality of linear logic is formulated in terms of integral between measures and measurable functions. The orthogonality embodies a simple reciprocity on kernels actions on measurable functions and measures. Following Hyland-Schalik's double gluing construction with tight orthogonality, we show that the free exponential of (I) is lifted to the tight orthogonal category over the s-finite kernels. To achieve this lifting, we rely the coherence of the limit with equalisers imposed by MTT, This coherence is shown to be realised through the Lebesgue monotone convergence theorem.
     Note that both (i) and (ii) do not incorporate any closed structure for monoidal products in the continuous framework, making them inconclusive as a complete model of linear logic.
</well>
</collapse>


[[en:seminaires:semantique:index|Semantics]]\\
Wednesday October 25, 2023, 10:45AM, Salle 3052, 3ème étage du bâtiment Sophie Germain\\
**Guillaume Geoffroy** (IRIF) //An introduction to integrable cones as a model of linear logic//
\\


[[en:seminaires:semantique:index|Semantics]]\\
Wednesday October 18, 2023, 10:45AM, Salle 3052, 3ème étage du bâtiment Sophie Germain\\
**Pierre Clairambault** (CNRS, Université d'Aix-Marseille) //From Thin Concurrent Games to Relational Models//
<button type="link" size="xs" collapse="b15-3249">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3249" collapsed="true">
<well size="sm">
Denotational models can roughly be classified in two kinds: static models (domains, relations, coherence spaces, etc), which record atemporal final "states" of completed executions; and dynamic models (game semantics, GoI, etc), which additionally describe how such final states are reached with temporal or causal information. The link between the two seems intuitively simple as it suffices to "forget time". But the question hides surprising conceptual depth and led to an active line of research in the 2000s, with landmark results by Melliès and Boudes among others.

Recently, there has been renewed interest in various extensions of relational models; either quantitative (e.g. the weighted relational model), or proof-relevant (e.g. distributors / generalized species of structure). In this talk, I will present recent results examining this dynamic-to-static question for such generalized relational models; in particular I will aim to arrive at a recent result obtained together with Olimpieri and Paquet: a cartesian closed pseudofunctor from the cartesian closed bicategory of thin concurrent games, to that of Fiore, Gambino, Hyland and Winskel's generalized species of structure.
</well>
</collapse>


[[en:seminaires:semantique:index|Semantics]]\\
Wednesday October 4, 2023, 10:45AM, Salle 3052, 3ème étage du bâtiment Sophie Germain\\
**Ryan Kavanagh** (McGill University) //Stable Semantics for Recursive Session-Typed Processes//
<button type="link" size="xs" collapse="b15-3250">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3250" collapsed="true">
<well size="sm">
Session-typed programming languages help programmers correctly
implement communicating systems. Though many techniques exist for
reasoning about these languages and their processes, few treat general
recursive types and few are compositional. As a consequence, they cannot
be applied to many useful programs and they do not support modular
reasoning. In this talk, I will present a denotational semantics for
Polarized Intuitionistic Processes (PIP), a session-typed
proofs-as-processes interpretation of polarized intuitionistic linear
logic. PIP features general recursion, channel transmission, choices,
and synchronization. This semantics generalizes Kahn’s semantics for
dataflow networks to support bidirectional, session-typed communication.
It supports modular reasoning and validates expected program
equivalences. Moreover, it is sound relative to barbed congruence (the
canonical behavioural notion of process equivalence), and it is fully
abstract in the absence of negative channel transmission. As a result,
our semantics provides an intuitively reasonable account of
session-typed communication and a foundation for reasoning about
processes in more realistic session-typed languages.
</well>
</collapse>


[[en:seminaires:semantique:index|Semantics]]\\
Tuesday July 25, 2023, 10:30AM, Salle 146 (Olympe de Gouges)\\
**Clovis Eberhart** (National Institute of Informatics (NII, Tokyo)) //A Compositional Approach to Parity Games//
<button type="link" size="xs" collapse="b15-3251">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3251" collapsed="true">
<well size="sm">
In this talk, I will introduce open parity games, which form
a compositional approach to parity games. On the syntactic level,
these open games are defined as string diagrams, and can be thought of
as traditional parity games augmented with open ends. Our goal is to
show that computing the set of winning positions in such a game can be
done compositionally on the string diagram. To this end, we introduce
a suitable semantics inspired by the work by Grellois and Melliès on
the semantics of higher-order model checking. This semantics coincides
with the notion of winning position when there are no open ends and
can be computed compositionally on the syntax.
</well>
</collapse>


[[en:seminaires:semantique:index|Semantics]]\\
Tuesday February 21, 2023, 10:30AM, Salle 1007\\
**Nima Rasekh** (Max Planck Institute in Mathematics (MPIM) Bonn) //Category Theory of Universes//
<button type="link" size="xs" collapse="b15-3252">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3252" collapsed="true">
<well size="sm">
A key concept of higher topos theory involves the existence of
universes, either by definition (in the elementary case) or by
construction (in the Grothendieck case). In this talk we want to
illustrate how comprehending the category theory of internal universes
could help us internalize a variety of key constructions. This would
allow us to obtain results known in the classical setting in an
elementary higher topos. No prior knowledge of higher category theory of
any form will be assumed.
</well>
</collapse>


[[en:seminaires:semantique:index|Semantics]]\\
Tuesday January 10, 2023, 11AM, Salle 1007\\
**Paul Ruet** (IRIF) //Asymptotic cones of groups and complexity//
<button type="link" size="xs" collapse="b15-3253">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b15-3253" collapsed="true">
<well size="sm">
Une introduction au problème du mot, lien entre sa complexité et la théorie géométrique des groupes, en particulier avec les cônes asymptotiques.
</well>
</collapse>