LHC days

LHC is a French workgroup about logic, homotopy and categories. The seventh edition of the LHC days will take place on Wednesday 17 and Thursday 18 June 2026 at LMF laboratory of Université Paris Saclay in Palaiseau.

It will be followed, on Friday 19 June 2026, by a colloquium in memoriam of Gilles Dowek.

Practical details

The conference will take place in room 1B36 at LMF laboratory of Université Paris Saclay in Palaiseau:

In order to come from Paris, you should take RER B train line (see RATP for schedules), stop at Massy Palaiseau and take the bus 5154 until Moulon stop (or bus 4609 from Le Guichet). The travel takes roughly 1 hour from Paris. You can have a look at the RATP website to schedule your trip, the schedule of the RER B train or the current status of the RER B.

It is possible to come by car and use the ENS parking lot: in this case, your license plate should be registered in advance by the organizers.

A lunch buffet should be provided to registered participants.

Social event. There is no formal social event, but we can gather at the Brass & Co pub nearby on Wednesday after the talks.

Invited speakers

• Sophie D’Espalungue (IRIF): Small, Strict, Internal, Enriched… Universes and the Grothendieck Construction across Internalised Enrichments
• Félix Loubaton (CNRS, amU): Double Toposes

Program

We provide an icalendar for the program.

Wednesday 17 June 2026

09:00	Welcome coffee
09:30	Niyousha Najmaei
	For Generalised Algebraic Theories, Two Sorts Are Enough
09:55	El Mehdi Cherradi
	Non-linear contexts and dependent operads
10:20	Arthur Adjedj
	AdapTT: Functoriality for Dependent Type Casts
10:45	Break
11:15	Yoann Barszezak
	Shapely monads for weak higher categories
11:40	Louise Leclerc
	A type theory for weak ω-categories
12:05	Rafaël Bocquet
	A General Cubical Framework for Coherence Theorems
12:30	Lunch
14:00	Félix Loubaton, Invited talk
	Double Toposes
15:00	Robin Jourde
	Relational theories and their locally presentable categories of models, with applications to skeletal semantics
15:25	Paul-André Melliès
	From ordinary to dependent presheaves, with an application to local stores
15:50	Break
16:20	Quentin Aristote
	Profunctorial algebras
16:45	Bruno Drieux
	Relative (co-)Yoneda Lemma for Categories Indexed over a Small-Generated Site
17:10	Manuel Catz
	Oriented Simplices and Cubes are Parametric
17:35	End of the day, beginning of the night

Thursday 18 June 2026

09:00	Welcome coffee
09:30	Aymeric Walch
	A recipe for web models of Linear Logic
09:55	Elies Harington
	Internal relational models of Linear Logic
10:20	Meven Lennon-Bertrand
	Bidirectional Interpolation for the λ-Calculus
10:45	Break
11:15	Victor Iwaniack
	Two-way and tree automata as functors
11:40	Yorgo Chamoun
	A compositional definition of automata
12:05	Luidnel Maignan
	Quotienting Sites of Open Sets
12:30	Lunch
14:00	Sophie D'Espalungue, Invited talk
	Small, Strict, Internal, Enriched... Universes and the Grothendieck Construction across Internalised Enrichments
15:00	Jonathan Weinberger
	The ∞-category of ∞-categories in simplicial type theory
15:25	Augustin Albert
	Homological Algebra in Abelian Framed Bicategories
15:50	Break
16:20	Arturo De Faveri
	An algebraic view on the linear lambda calculus
16:45	Lutz Straßburger
	Proof Identity and Categorical Models of BV
17:10	Thomas Perez
	Axiomatizing Fermionic Circuits: From Premonoidal Semantics to Monoidal Theories with Non-Natural Symmetry
17:35	End of the days

Abstracts

Arthur Adjedj (ENS Paris-Saclay, Université Paris-Saclay)
AdapTT: Functoriality for Dependent Type Casts [slides]

The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural behavior that boils down to the pervasive functoriality of type formers. We propose and extensively study a type theory, called AdapTT, which makes systematic and precise this idea of functorial type formers, with respect to an abstract notion of adapters relating types. Leveraging descriptions for functorial inductive types in AdapTT, we derive structural laws for type casts on general inductive type formers.

Augustin Albert (LIX)
Homological Algebra in Abelian Framed Bicategories [slides]

We introduce abelian framed bicategories, which are particular framed bicategories that are locally abelian, and show that they are suitable for developing homology and cohomology theories for directed structures. This means in particular that similar exact sequences as the relative homology and Mayer–Vietoris long exact sequences can be shown to hold. Also, for closed monoidal abelian framed bicategories, Künneth theorem holds as well. Finally, we prove embedding theorems similar to the Gabriel and Freyd–Mitchell theorems, for particular abelian framed bicategories, allowing to see those as bicategories of bimodules over algebras. This naturally links to the original motivation of this work, which was to generalize directed homology developed in the abelian framed bicategory of bimodules over (path) algebras.

Quentin Aristote (IRIF, Université Paris-Cité)
Profunctorial algebras [slides]

We provide a bicategorical generalization of Barr’s landmark 1970 paper, in which he describes how to extend Set-monads to relations and uses this to characterize topological spaces as the relational algebras of the ultrafilter monad. With two-sided discrete fibrations playing the role of relations in a bicategory, we first characterize, in terms of exact squares, when pseudomonads on a bicategory extend to its bicategory of two-sided discrete fibrations. As a wide class of examples, we show that every Set-monad induces a pseudomonad on the 2-category of categories satisfying our criterion and thus extending to profunctors. Among these, we then focus on the ultracompletion pseudomonad, whose pseudoalgebras are ultracategories: we characterize the normalized lax algebras of its profunctorial extension as ultraconvergence spaces, a recently-introduced categorification of topological spaces.

Yoann Barszezak (IRIF)
Shapely monads for weak higher categories

The definitions of some algebraic structures, like multicategories, polycategories, PROPs, or properads, are easily sketched with a few pictures on a board. Garner and Hirschowitz introduced shapely monads for producing intuitive alternative definitions of such algebraic structures, essentially from pictures, as follows.

1. Pictures are presheaves over a suitable base category.
2. By saturating pictures under “substitution” one obtains a class of “allowed” shapes.
3. One generates a monad based on homming out of allowed shapes, the “free shapely monad”. Shapeliness means that the monad has at most one operation of each arity (=shape).
4. The relevant algebraic structures are algebras for the obtained monad.

However, Garner and Hirschowitz merely defined shapely monads in a few concrete settings, i.e., for a few base categories. In this talk, we present work towards a more abstract and general definition of shapely monads, and construction of free ones. We illustrate the construction on bicategories, and sketch how it could lead to a shapely monad for weak higher categories.

Rafaël Bocquet (Inria, LS2N, Gallinette)
A General Cubical Framework for Coherence Theorems [slides]

I will present a general framework for the general study of coherence and strictification theorems. This takes place at the level of an equational extension of generalized algebraic theories, comparing a weak theory (e.g. monoidal categories) with a strict theory (e.g. strict monoidal categories). In this setting, strictification says that the weak and strict theories present the same homotopy theory. Meanwhile coherence says that certain ∞-groupoids are 0-truncated. The main result is then that, assuming that the two theories have sufficiently well-behaved homotopy theories, coherence implies strictification. The ∞-groupoids that are involved are explicitly described as cubical sets. This work is mainly motivated by applications to equational extensions of dependent type theories, where some conservativity results are known to hold in the presence of the uniqueness of identity proofs principle (UIP) and conjectured in its absence.

Manuel Catz (IRIF)
Oriented Simplices and Cubes are Parametric

Street’s Orientals construction provides a structure of $n$-(strict) category to the $n$-simplex $\Delta_n$ via the functor $\mathcal{O}: \Delta \to \omega Cat$. Recent work by Ara, Lafont and Métayer show how $\mathcal{O}_n$ can be seen as a free category on a polygraph of which the generators can be inductively generated. Likewise, we propose a similar construction of oriented cubes and analyze their relation to the oriented simplices following insights found in the work of Aitchison. Both the simplicial and cubical case can be regrouped into a common framework, the one of Reynolds’ parametricity, specifically the iteration of its unary and binary variants, as seen in the work of Herbelin and Ramachandra. The main contribution is to offer an approach leveraging unified notation and thus building well-defined translations between these two variants. This is ongoing work with Hugo Herbelin and François Métayer.

Yorgo Chamoun (LIX, École polytechnique)
A compositional definition of automata [slides]

It is famously known that the language recognized by an automaton and the operation of composition of automata behave poorly with respect to each other. Historically, this has been handled by adding silent transitions to the formalism of automata theory, which provably gives an equivalent theory in terms of expressivity. For example, this is used in the proof of Kleene’s Theorem, relating languages recognized by finite automata and rational expressions. We adopt a completely different point of view: in order to make automata theory compositional, we simply identify the categorical operations that are necessary to build all automata, and we consider the free category with these operations. More precisely, we consider the free loop-free traced symmetric monoidal category containing a qualitative bialgebra and the alphabet as endomorphisms. Then we characterize this category as a symmetric monoidal category whose objects are natural numbers, and whose morphisms from m to n are automata with m inputs and n outputs. The category Aut of automata thus obtained is compositional with respect to the language, in the sense that we can define the operation that associates to an automaton the language it recognizes as a functor on Aut, which sheds new lights on this operation.

El Mehdi Cherradi (IRIF, CNRS)
Non-linear contexts and dependent operads [slides]

In type theory, contexts are usually represented by finite list of types (with possible dependencies). We propose a framework allowing any finite poset to be the shape of a context, where the order accounts for the dependencies. This allows a formulation of dependent operads, in a fibered way as introduced by Lurie, as collections of operations whose inputs (and outputs) are dependently typed. We provide general definitions for such objects and their algebras, for which the typical examples consists of GATs and their models, and discuss some properties, including monadicity of algebras over “dependent” sets.

Sophie D’Espalungue (IRIF)
Small, Strict, Internal, Enriched… Universes and the Grothendieck Construction across Internalised Enrichments

I will discuss the notion of smallness introduced in my thesis, defined in the context of a recursive hierarchy 𝕋ₙ : 𝕋ₙ₊₁ (n ≥ -3) whose most basic instance is that of the (n+1)-category of n-categories. This allows for talking about an r-small n-category for r ≤ n without relying on an external set-theoretical framework such as ZF. A topos ℰ, along with its subobject classifier Ω, equipped with its element ⊤ representing truth, gives another instance of such a formal hierarchy. It starts with ⊤ : Ω : ℰ : 𝗖𝗔𝗧 : 𝗖𝗔𝗧₂ : …. In this view, one can think of the first n levels of such a hierarchy as an n-topos. To motivate this notion of size, I will focus on the formal category theory developed in this context (roughly, n ≤ 2) and arising from an internalisation of the notion of enrichment [d’E23, Ch. I]. I will also use some work in progress. Notably, I will discuss how the Grothendieck construction interacts with smallness, and give examples of small objects in this context. The overall objective is to provide another view on the role and the structure of universes, and so I will display the objects considered throughout, by their position on a map structuring HoTT-like universe hierarchies.

Arturo De Faveri (IRIF, Université Paris Cité)
An algebraic view on the linear lambda calculus [slides]

The aim of the talk is to report on ongoing work to investigate the linear fragment of the λ-calculus using the tools of categorical universal algebra, adapting techniques and ideas developed by Hyland to the linear setting of operads and monoidal categories. We start by investigating algebraic models of the linear λ-calculus through the notion of semiclosed operad and we prove that each of such models gives rise to a linear reflexive object in a closed monoidal category. Inspired by the notion of λ-algebra, we define a category of linear λ-algebras, and we prove that this category is equivalent to that of semiclosed operads. Therefore, combining the two results, we have that every linear λ-algebra gives rise to a linear reflexive object in a closed monoidal category.

Bruno Drieux (Grothendieck Institute, École Polytechnique)
Relative (co-)Yoneda Lemma for Categories Indexed over a Small-Generated Site [slides]

It is well known that the internal logic of a (Grothendieck) topos can be used to make it look like the category of sets. Moving to higher category theory, one should expect that the internal language of a 2-category of stacks over a small-generated site could be used to make it look like the 2-category of (locally small) categories. However, a formal language and metatheorems suited to this purpose have yet to be fully worked out. To this end, we develop some fundamental notions and results of the theory of categories indexed over a small-generated site. In particular, we associate to any (essentially small) indexed category a collection of indexed representable presheaves which defines an indexed Yoneda functor to the corresponding indexed category of indexed presheaves. We then prove an indexed version of the Yoneda lemma, as well as an indexed version of the co-Yoneda lemma, meaning a representation theorem of indexed presheaves as indexed colimits of indexed representable presheaves.

Elies Harington (University of Nottingham)
Internal relational models of Linear Logic [slides]

The category of sets and relations is the prototypical model of Linear Logic, and the basis for many generalizations: coherence spaces, finiteness spaces, weighted relations… In this talk we propose yet another generalization of the relational model: under suitable conditions, the category of relations internal to some category C can be endowed with the structure of a model of Linear Logic. We explain the philosophy that led to this main result, give a few examples of such models and conclude with possible generalizations related to spans and profunctor-based bicategorical models of linear logic.

Victor Iwaniack (Université Aix-Marseille)
Two-way and tree automata as functors [slides]

A deterministic automaton is a formal machine whose goal is to accept (“recognise”) or reject a word (a finite sequence of symbols) using a simple procedure. To each automaton we associate a set of words, called a language, recognised by this automaton. In their article [1], Colcombet and Petrişan give a description of languages and automata as functors; in this framework, recognition becomes extension of the language-as-a-functor by an automaton-as-a-functor. They also show how the classical result of minimisation of automata can be retrieved using purely categorical tools such as Kan extensions and orthogonal factorisation systems. In this talk, I will give two new types of automata that we can see as functors: two-way automata and tree automata. For the former, we use the functorial viewpoint to categorically deduce a “Shepherdson construction” turning a two-way automaton into a one-way automaton. For the latter, reading trees instead of words, we adapt the functorial minimisation process to retrieve minimisation of tree automata.

[1] Thomas Colcombet and Daniela Petrişan. “Automata Minimization: A Functorial Approach”. In: Logical Methods in Computer Science 16.1 (Mar. 2020), Issue 1, 18605974. DOI: 10.23638/LMCS-16(1:32)2020.

[2] Victor Iwaniack. “Automates topossiques”. Thèse de Doctorat. Université Côte d’Azur, June 2025. DOI: 10.70675/db751a45zd591z4819za546z64d602ae7d91

Robin Jourde (Université Savoie Mont Blanc)
Relational theories and their locally presentable categories of models, with applications to skeletal semantics [slides]

We study virtual double theories, which are a virtual-double-categorical extension of Lawvere theories, allowing for the interpretation of some morphisms as relations. We first prove that the category of models of any virtual double theory is locally presentable. We then introduce a notion of presentation for virtual double theories, analogous to the notion of presentation of a Lawvere theory by generators and relations. Finally, we apply these results to design a mathematical foundation for skeletal semantics, a software framework for specifying and analysing programming languages. We show that skeletal specifications may be interpreted as presentations of virtual double theories, so that the category of models of the virtual double theory associated to any presentation provides the intended language with initial algebra semantics.

Louise Leclerc (LIX, Polytechnique)
A type theory for weak ω-categories [slides]

We present a type theory modeled by the ∞-topos of presheaves over the category Θ. In particular, we may carve out a type of weak (∞,ω)-categories by defining suitable Segal and completeness conditions. In many regards the approach we take follows the ideas introduced by E. Riehl and M. Shulman in their Simplicial Type Theory.

Meven Lennon-Bertrand (INRIA – IRIF, Université Paris Cité)
Bidirectional Interpolation for the λ-Calculus [slides]

With Alexis Saurin, we have been revisiting a proof-relevant version (for the λ-calculus) of interpolation, a property dear to proof theorists. The original proof, due to Čubrić, looks rather messy on the surface, but its underlying structure is very neat, and exposing it brought up an interesting (and, to me, new) connection in the Curry-Howard spirit between the subformula property and bidirectional typing.

Félix Loubaton (CNRS, amU)
Double Toposes

One perspective on (Grothendieck) toposes is to view them as a place where we can perform a “set-like” theory. The question of identifying place to do a “category-like” theory then arises naturally. (One of the) answer is provided by the notion of double topos. After a brief introduction recalling the definition of toposes, we will define double categories and present some of their properties. Finally, we will introduce double toposes and state a double categorical Giraud theorem. This results are part of a work in progress in collaboration with Jaco Ruit.

Luidnel Maignan (LACL / Université Paris-Est Créteil)
Quotienting Sites of Open Sets

Many years ago, with application to cellular automata theory in mind, we did an attempt at quotienting a site because the quotient of the underlying topological spaces was non-satisfactory. Coming back to this subject recently with more knowledge on those topics, we’ve been able to make it rigorous and compare it with known constructions (e.g. Grothendieck construction, lax colimit, points of topoi, topological groupoids, equivariant sheaves)

Paul-André Melliès (CNRS)
From ordinary to dependent presheaves, with an application to local stores

We generalize ordinary presheaves over a category B into a fibrational notion of dependent presheaf defined as sections of a specific functor p : E → B of interest. We then develop a theory of dependent left Kan extensions unifying both cartesian liftings and ordinary Kan extensions. We show how to factor the local state monad into a sequence of two adjunctions and an equivalence between categories of dependent presheaves. We then show that the composite adjunction is monadic, which means that the category of algebras of the local state monad coincides with a category of presheaves in our extended dependent sense.

Niyousha Najmaei (LIX, École Polytechnique)
For Generalised Algebraic Theories, Two Sorts Are Enough [slides]

Generalised algebraic theories (GATs) allow multiple sorts indexed over each other. For example, the theories of categories or Martin-Löf type theories form GATs. Categories have two sorts, objects and morphisms, and the latter are double-indexed over the former. Martin-Löf type theory has four sorts: contexts, substitutions, types and terms. For example, types are indexed over contexts, and terms are indexed over both contexts and types. In this paper we show that any GAT can be reduced to a GAT with only two sorts, and there is a section-retraction correspondence (formally, a strict coreflection) between models of the original and the reduced GAT. In particular, any model of the original GAT can be turned into a model of the reduced (two-sorted) GAT and back, and this roundtrip is the identity. The reduced GAT is simpler than the original GAT in the following aspects: it does not have sort equalities; it does not have interleaved sorts and operations; if the original GAT did not have interleaved sorts and operations, then the reduced GAT won’t have operations interleaved between different sorts. In a type-theoretic metatheory, the initial algebra of a GAT is called a quotient inductive-inductive type (QIIT). Our reduction provides a way to implement QIITs with sort equalities or interleaved constructors which are not allowed by Cubical Agda. An instance of our reduction is the well-known method of reducing mutual inductive types to a single indexed family. Our approach is semantic in that it does not rely on a syntactic description of GATs, but instead, on Uemura’s bi-initial characterisation of the category of (finite) GATs in the 2-category of finitely complete categories with a chosen exponentiable morphism.

This is Joint work with Samy Avrillon, Ambrus Kaposi, Ambroise Lafont and Johann Rosain. A preprint is available at https://arxiv.org/abs/2601.19426.

Thomas Perez (INRIA Saclay)
Axiomatizing Fermionic Circuits: From Premonoidal Semantics to Monoidal Theories with Non-Natural Symmetry

Fermionic computing is a variation of quantum computing where the information is carried by a particular kind of particle: Fermions. Those particules are fundamentally indistinguishible, meaning that two Fermions cannot be told apart from one another. This has consequences on their statistics, which are modeled in the physical theories by a non trivial behaviour under permutation of these indistinguishable entities. In practice, it implies that fermionic computations behave very much like effectful computations for a non-commutative monad. In this paper we study the denotational semantics of fermionic computing using symmetric premonoidal categories. We show that in this specific case we can equivalently work in a pre-symmetric monoidal category, that is a monoidal category aquipped with a non-natural symmetry. From this point, we move on providing universal and complete diagrammatical syntaxes for various fragments of fermionic computing by extending the theory of scalable notations and matrix arrows from the symmetric to the pre-symmetric setting.

Lutz Straßburger (Inria & LIX)
Proof Identity and Categorical Models of BV

BV-categories are a recent development that aims to give categorical semantics to proofs in the logic BV. However, due to the absence of a coherence theorem on one side and a well-defined notion of proof identity for BV on the other side, the precise relation between BV-categories and the logic BV is still not clear. To improve on this situation, we define a notion of proof identity for BV, based on the notion of atomic flows, which can be seen as a special form of string diagrams. Based on this notion of proof identity, we then strengthen the existing notion of BV-category and prove that it is sound with respect to the logic.

Joint work with Matteo Acclavio and Vladimir Zamdzhiev

Aymeric Walch (ISAE-SUPAERO)
A recipe for web models of Linear Logic [slides]

I describe in this talk a generic construction of web models of linear logic with partial sums. This construction captures a wide class of orthogonality models, ranging from coherence spaces to probabilistic coherence spaces, finiteness spaces and Köthe spaces.

All these models are built on the same principles, but were very heterogeneous in the specificities of their technical development. This construction factorizes these specificities, allowing a unified treatment of further developments, such as differentiation and Taylor expansion.

Jonathan Weinberger (Chapman University)
The ∞-category of ∞-categories in simplicial type theory

Simplicial type theory (STT) was introduced by Riehl and Shulman to leverage homotopy type theory to prove results about (∞,1)-categories. Initial work on simplicial type theory focused on “formal” arguments in higher category theory and, in particular, no non-trivial examples of ∞-category theory were constructible within STT. More recent work has changed this state of affairs by applying techniques developed initial for cubical type theory to construct the ∞-category of spaces. We complete this process by constructing the ∞-category of ∞-categories, recovering one of the main foundational results of ∞-category theory (straightening–unstraightening) purely type-theoretically. We also show how this construction enables new examples of the directed version of the structure identity principle, the structure homomorphism principle. This is joint work (https://arxiv.org/abs/2602.02218) with Daniel Gratzer and Ulrik Buchholtz

Participants

1. Arthur Adjedj (ENS Paris-Saclay, Université Paris-Saclay)
2. Wass Ait Moussa (INRIA - IRIF )
3. Augustin Albert (LIX)
4. Quentin Aristote (IRIF, Université Paris-Cité)
5. Yoann Barszezak (IRIF)
6. Thibaut Benjamin (Université Paris-Saclay)
7. Rafaël Bocquet (Inria, LS2N, Gallinette)
8. Ewen Broudin-Caradec (LMF)
9. Titouan Carette (École polytechnique)
10. Manuel Catz (IRIF)
11. Yorgo Chamoun (LIX, École polytechnique)
12. El Mehdi Cherradi (IRIF, CNRS)
13. Emily Clement (CNRS, LIPN)
14. Simon Corbard (ENS Paris Saclay)
15. Pierre-Louis Curien (IRIF)
16. Helder Da Costa ()
17. Ishan Dasgupta Samarendra (University of Cambridge)
18. Rashiqa Dawood (Université Sorbonne Paris Nord )
19. Arturo De Faveri (IRIF, Université Paris Cité)
20. Bruno Drieux (Grothendieck Institute, École Polytechnique)
21. Jérémy Dubut (LIX)
22. Aloÿs Dufour (Université Paris Nord)
23. Thomas Ehrhard (IRIF CNRS)
24. Uli Fahrenberg (LMF)
25. Simon Forest (LORIA)
26. Jonas Frey (LIPN - USPN)
27. Zoé Garreau (ENS Lyon)
28. Pierre Giraud ()
29. Jean Goubault-Larrecq (LMF)
30. Léonard Guetta (Universiteit Utrecht)
31. Francesca Guffanti (Universite’ Savoie Mont Blanc)
32. Elies Harington (University of Nottingham)
33. Maya Hayman (ENS de Lyon)
34. Simon Henry (University of Ottawa)
35. Hugo Herbelin (IRIF - Inria)
36. Ryan Hota (Chennai Mathematical Institute )
37. Victor Iwaniack (Université Aix-Marseille)
38. Maxime Joubert (École polytechnique, LIX)
39. Robin Jourde (Université Savoie Mont Blanc)
40. Moana Jubert (Université Paris-Cité)
41. Tommy-Lee Klein (Institut de mathématiques de Marseille )
42. Jad Koleilat (LIPN)
43. Yves Lafont (Institut de Mathématiques de Marseille)
44. Ambroise Lafont (Ecole Polytechnique)
45. François Lamarche (INRIA (retired))
46. Thomas Laure (LIPN )
47. Sacha Le Hir Mazé (École polytechnique )
48. Serge Lechenne (ENS ULM)
49. Louise Leclerc (LIX, Polytechnique)
50. Jérémy Ledent (IRIF, Université Paris Cité)
51. Meven Lennon-Bertrand (INRIA – IRIF, Université Paris Cité)
52. Leopoldo Lerena (Universidad de Buenos Aires)
53. Félix Loubaton (CNRS, amU)
54. Noah Loutchmia ()
55. Elsa Lubek (IRIF)
56. Luidnel Maignan (LACL / Université Paris-Est Créteil)
57. Georges Maltsiniotis ()
58. Paul-André Melliès (CNRS)
59. Samuel Mimram (École polytechnique)
60. François Métayer (IRIF)
61. Niyousha Najmaei (LIX, École Polytechnique )
62. Frédéric Paugam (Sorbonne Université)
63. Thomas Perez (INRIA Saclay)
64. Vincent Peth (ENS PSL)
65. Alexis Pocquet (Institut Polytechnique de Paris)
66. Stiéphen Pradal (University of Nottingham)
67. Antoine Spicher (LACL - Université Paris Est Créteil)
68. Lutz Straßburger (Inria & LIX)
69. Aymeric Walch (ISAE-SUPAERO)
70. Jonathan Weinberger (Chapman University)
71. Théo Winterhalter (LMF, INRIA Saclay)
72. Jean Zablocki (CNRS, Université Paris-Cité, IRIF)
73. Noam Zeilberger (Ecole Polytechnique)
74. Sophie d’Espalungue (IRIF, Université Paris-Cité)
75. Sam van Gool (ENS Paris-Saclay)

Related events

• Colloque en hommage à Gilles Dowek

Contacts

In case of any question, you can contact the organizers

• local organizers: Thibaut Benjamin and Uli Fahrenberg
• LHC coordinators: Samuel Mimram and Lionel Vaux

Support