My Publications

 

Publications

Higher Category Theory

Papers

  • Invertible cells in ω-categories. Thibaut Benjamin and Ioannis Markakis. 2024.
    We study coinductive invertibility of cells in weak ω-categories. We use the inductive presentation of weak ω-categories via an adjunction with the categroy of computads, and show that invertible cells are closed under all operations of ω-categories. Moreover, we give a simple criterion for invertibility in computads, together with an algorithm computing the data witnessing the invertibility, including the inverse, and the cancellation data.
  • CaTT contexts are finite computads. Thibaut Benjamin and Ioannis Markakis and Chiara Sarti. 2024.
    Two novel descriptions of weak ω-categories have been recently proposed, using type-theoretic ideas. The first one is the dependent type theory CaTT whose models are ω-categories. The second is a recursive description of a category of computads together with an adjunction to globular sets, such that the algebras for the induced monad are again ω-categories. We compare the two descriptions by showing that there exits a fully faithful morphism of categories with families from the syntactic category of CaTT to the opposite of the category of computads, which gives an equivalence on the subcategory of finite computads. We derive a more direct connection between the category of models of CaTT and the category of algebras for the monad on globular sets, induced by the adjunction with computads.
  • Opposites of weak ω-categories and the suspension and hom adjunction. Thibaut Benjamin and Ioannis Markakis. 2024.
    We define inductively the opposites of a weak globular ω-category with respect to a set of dimensions, and we show that the properties of being free on a globular set of a computad are preserved under forming opposites. We then provide a new description of hom ω-categories, and show that the opposites of a hom ω-category are hom ω-category of opposites of the original ω-category.
  • Formalisation of Dependent Type Theory: The Example of CaTT. Benjamin, Thibaut. In 27th International Conference on Types for Proofs and Programs (TYPES 2021), Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, Basold, Henning and Cockx, Jesper and Ghilezan, Silvia, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, pages: 2:1–2:21, 2022.
    We present the type theory CaTT, originally introduced by Finster and Mimram to describe globular weak ω-categories, and we formalise this theory in the language of homotopy type theory. Most of the studies about this type theory assume that it is well-formed and satisfy the usual syntactic properties that dependent type theories enjoy, without being completely clear and thorough about what these properties are exactly. We use the formalisation that we provide to list and formally prove all of these meta-properties, thus filling a gap in the foundational aspect. We discuss the key aspects of the formalisation inherent to the theory CaTT, in particular that the absence of definitional equality greatly simplify the study, but also that specific side conditions are challenging to properly model. We present the formalisation in a way that not only handles the type theory CaTT but also all the related type theories that share the same structure, and in particular we show that this formalisation provides a proper ground to the study of the theory MCaTT which describes the globular, monoidal weak ω-categories. The article is accompanied by a development in the proof assistant Agda to actually check the formalisation that we present.
  • Monoidal weak ω-categories as models of a type theory. Benjamin, Thibaut. In Mathematical Structures in Computer Science, Cambridge University Press, pages: 1–37, 2022.
    Weak ω-categories are notoriously difficult to define because of the very intricate nature of their axioms. Various approaches have been explored based on different shapes given to the cells. Interestingly, homotopy type theory encompasses a definition of weak ω-groupoid in a globular setting, since every type carries such a structure. Starting from this remark, Brunerie could extract this definition of globular weak ω-groupoids, formulated as a type theory. By refining its rules, Finster and Mimram have then defined a type theory called 𝖢𝖺𝖳𝖳 , whose models are weak ω-categories. Here, we generalize this approach to monoidal weak ω-categories. Based on the principle that they should be equivalent to weak ω-categories with only one 0-cell, we are able to derive a type theory 𝖬𝖢𝖺𝖳𝖳 whose models are monoidal weak ω-categories. This requires changing the rules of the theory in order to encode the information carried by the unique 0-cell. The correctness of the resulting type theory is shown by defining a pair of translations between our type theory 𝖬𝖢𝖺𝖳𝖳 and the type theory 𝖢𝖺𝖳𝖳 . Our main contribution is to show that these translations relate the models of our type theory to the models of the type theory 𝖢𝖺𝖳𝖳 consisting of ω-categories with only one 0-cell by analyzing in details how the notion of models interact with the structural rules of both type theories.
  • Globular weak ω-categories as models of a type theory. Benjamin, Thibaut and Finster, Eric and Mimram, Samuel. 2024.
    Accepted in Higher Structures
    We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak ω-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak ω-categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak ω-groupoids: those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an ω-category. This comparison is established by proving the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for a certain class of dependent type theories
  • Globular weak ω-categories as models of a type theory. Benjamin, Thibaut and Finster, Eric and Mimram, Samuel. 2021.
    Accepted at the workshop on Homotopy Type Theory / Univalent Foundations
  • Suspension et Fonctorialité: Deux Opérations Implicites Utiles en CaTT. Benjamin, Thibaut and Mimram, Samuel. In Journées Francophones des Langages Applicatifs, 2019.
    In French
    La notion de ω-catégorie faible est une vaste généralisation de celle de catégorie, qui revêt une importance croissante en mathématiques. Cependant, les définitions qui en ont été proposées à ce jour à ce jour restent difficiles à manipuler en pratique : on ne connaît pas de liste explicite des cohérences qui doivent être présentes dans ces structures et il devient rapidement difficile de vérifier tous les détails qui doivent l’être lors de leur utilisation. Partant de ce constat, Finster et Mimram ont récemment reformulé la définition de Grothendieck et Maltsiniotis des ω-catégories faibles sous forme d’une théorie des types, appelée CaTT. Ceci a posé les bases d’un assistant de preuve, développé par les auteurs, dans lequel les termes typables sont ceux qui correspondent à des cohérences. La formalisation de preuves non-triviales dans ce système a montré la nécessité d’avoir des outils permettant de les automatiser en partie. Dans cette optique, nous présentons ici deux méthodes permettant de générer automatiquement des cohérences de dimension supérieure à partir de cohérences existantes : la suspension et la fonctorialité. Nous montrons qu’elles sont admissibles (c’est-à-dire que leur présence ne modifie pas le pouvoir expressif de la théorie des types) et qu’elles sont utiles en pratique pour alléger les preuves en évitant des redondances.
  • My PhD Thesis

  • A type theoretic approach to weak omega-categories and related higher structures. Benjamin, Thibaut. 2020.
    We study a type theoretic definition of weak omega-categories originally introduced by Finster and Mimram, inspired both from ideas coming from homotopy type theory and from a definition of weak omega-category due to Grothendieck and Maltsiniotis. The advantages of such an approach are multiple: The language of type theory allows for a definition restricted to only a few rules, it also provides an explicit syntax on which one can perform inductive reasoning, and gives an algorithm for implementing a proof-assistant dedicated to exploring weak omega-categories. The work we present about this type theory is organized along two main axes: We investigate the theoretical grounds for this definition and relate it to an other known definition of weak omega-categories, and we present the proof-assistant based on this theory together with practical considerations to improve its use. We also consider a generalization of this approach to other related higher structures.We start with an introduction to the language of dependent type theory that we rely on to introduce our definitions, presenting both the syntax and the semantics that we study by means of categorical tools. We then present weak omega-categories and a type theory that defines them. We detail the categorical semantics of this theory and our main contribution in this direction establishes an equivalence between its models and the prior definition of weak omega-categories due to Grothendieck and Maltsiniotis. This definition has enabled us to implement a proof-assistant capable of checking whether a given morphism is well-defined in the theory of weak omega-category, and we present this implementation together with a few examples demonstrating both the capabilities of such a tool, and its tediousness in the vanilla version. To improve this issue, we present two main additional features allowing to partially automating its use: The suspension and the functorialization. These two operations are defined by similar techniques of induction on the syntax of the type theory. We then generalize this definition of weak omega-categories and present a type theoretic framework that is both modular enough to allow for defining higher structures, and constrained enough to precisely understand its semantics. This enables us to sketch a connection with the theory of monads with arities. Using this framework, we introduce and study two other definitions of higher structures: Monoidal weak omega-categories and cubical weak omega-categories. By using syntactic reasoning we are able to defines translations back and forth between the type theory defining weak omega-categories and the one describing monoidal weak omega-categories. One of our main result is to show that these translations imply an equivalence at the level of models: It shows that the monoidal omega-categories are equivalent to the omega-categories with a single object thus justifying the correctness of the appellation monoidal. We then give an alternate presentation of the type theory defining monoidal weak omega-categories, which diverges from our framework but is more standalone, and prove it to be equivalent to the previous presentation. We finally introduce in our framework a definition of cubical weak omega-categories and study its semantics, our main result along these lines is to characterize the models of this type theory and extract a mathematical definition equivalent to them.
  • Runtime Assertion Checking

  • Abstract Interpretation of Recursive Logic Definitions for Efficient Runtime Assertion Checking. Benjamin, Thibaut and Signoles, Julien. In International Conference on Tests and Proofs (TAP), Best Paper Award. 2023.
    Runtime Assertion Checking (RAC) is a lightweight formal method for verifying at runtime code properties written in a formal specification language. One of the main challenge of RAC is to check the properties efficiently, while emitting sound verdicts. In particular, arithmetic properties are only efficiently verified using machine integers, yet soundness can only be achieved by using an exact but slower exact arithmetic library. This paper presents how E-ACSL, a RAC tool for C programs, applies abstract interpretation for efficiently and soundly supporting arithmetic properties. Abstract interpretation provides sound static information regarding the size of terms involved in runtime assertions in order to choose at compile time whether machine integers or exact arithmetic will be used at runtime on a case by case basis. Our specification language includes recursive user-defined logic functions and predicates, for which we rely on fast fixpoint operators based on widening of abstract values.
  • Formalizing an Efficient Runtime Assertion Checker for an Arithmetic Language with Functions and Predicates. Benjamin, Thibaut and Signoles, Julien. In Symposium On Applied Computing (SAC), 2023.
    Runtime Assertion Checking (RAC) is a lightweight formal method that verifies formal code annotations, typically assertions, at runtime. The main RAC challenge consists in generating code that is both sound and efficient for checking expressive properties. In particular, checking formal arithmetic properties usually requires to use machine integer arithmetic to be efficient, but needs to rely on an exact yet slower arithmetic library to be sound. This paper formalizes an efficient RAC tool for arithmetic properties, which may include user-defined functions and predicates. Efficient code generation for these routines is based on specialization, allowing to generate efficient functions using machine arithmetic when possible, or slower functions relying on exact arithmetic, according to the calling context. This formalization is implemented in E-ACSL, a runtime assertion checker for C programs.
  • Formalisation d’un vérificateur efficace d’assertions arithmétiques à l’exécution. Benjamin, Thibaut and Ridoux, Félix and Signoles, Julien. In Journées Francophones des Langages Applicatifs (JFLA’22), 2022.
    In French
    La vérification d’assertions à l’exécution est une technique consistant à vérifier la validité d’annotations formelles pendant l’exécution d’un programme. Bien qu’ancienne, cette technique reste encore peu étudiée d’un point de vue théorique. Cet article contribue à pallier ce manque en formalisant un vérificateur d’assertions à l’exécution pour des propriétés arithmétiques entières. La principale difficulté réside dans la modélisation d’un générateur de code pour les propriétés visées qui génère du code à la fois correct et efficace. Ainsi, le code généré repose sur des entiers machines lorsque le générateur peut prouver qu’il est correct de le faire et sur une bibliothèque spécialisée dans l’arithmétique exacte, correcte mais moins efficace, dans les autres cas. Il utilise pour cela un système de types dédié. En outre, la logique considérée pour les propriétés inclue des constructions d’ordre supérieur. L’article présente également une implémentation de ce générateur de code au sein d’E-ACSL, le greffon de Frama-C dédié à la vérification d’assertions à l’exécution, ainsi qu’une première évaluation expérimentale démontrant empiriquement l’efficacité du code généré.
  •