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.

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

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.