Rencontre, 30 avril 2026
Programme
- 10:30 – 11:45
-
Simon Castellan (Épicure, INRIA)
In this talk, I will present the field of Science and Technology Studies (STS). Born in the 1970s at the crossroad between epistemology, sociology and history, the field proposes to enrich traditional philosophy of science by including the scientists as humans and members of society in the analysis. The goal of the talk is to illustrate how this field can provide us reflexivity on our own research and its interaction with society.
I will introduce the starting point of STS by briefly addressing the well-known problem of science neutrality. I will draw three areas of STS to illustrate how a change of perspective may alter the way of we do research and generate interesting research questions in computer science that may be more aligned with our values. Examples will be drawn from Botascopia, an interdisciplinary research between computer scientists, biologists and social scientists, using plant identification as a place to experiment different relationships between humans, nature and technology.
- 13:45 – 14:45
-
Niyousha Najmaei (LIX, École Polytechnique)
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories. We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.
This is joint work with Niels van der Weide, Benedikt Ahrens, and Paige Randall North.
Paper available at https://arxiv.org/abs/2503.10868
- 15:15 – 16:15
-
Thiago Felicissimo (Galinette, INRIA)Invited talk: Definitional Proof Irrelevance Made Accessible
A universe of propositions equipped with definitional proof irrelevance constitutes a convenient medium to express properties and proofs in type-theoretic proof assistants such as Lean, Rocq, and Agda. However, allowing accessibility predicates—used to establish semantic termination arguments—to inhabit such a universe yields undecidable typechecking, hampering the predictability and foundational bases of a proof assistant. To effectively reconcile definitional proof irrelevance and accessibility predicates with both theoretical foundations and practicality in mind, we describe a type theory that extends the Calculus of Inductive Constructions featuring observational equality in a universe of strict propositions, and two variants for handling the elimination principle of accessibility predicates: one variant safeguards decidability by sticking to propositional unfolding, and the other variant favors flexibility with definitional unfolding, at the expense of a potentially diverging typechecking procedure. Crucially, the metatheory of this dual approach establishes that any proof made in the definitional variant of the theory can be translated into a proof of the same statement in the propositional variant, all while preserving the decidability of the latter. Moreover, we prove the two variants to be consistent and to satisfy forms of canonicity, ensuring that programs can indeed be properly evaluated. We present an implementation in Rocq and compare it with existing approaches. Overall, this work introduces an effective technique that informs the design of proof assistants with strict propositions, enabling local computation with accessibility predicates without compromising the ambient type theory.
This is joint work with Yann Leray, Loïc Pujet, Nicolas Tabareau, Éric Tanter and Théo Winterhalter.
