A type theoretic approach to weak w-categories and related higher structures. (Catégories faibles et structures supérieures afférentes en théorie des types). - Thibaut Benjamin (2020)

Formalisation of Dependent Type Theory: The Example of CaTT. - Thibaut Benjamin (TYPES, 2021)

Globular weak ω-categories as models of a type theory. - Thibaut Benjamin; Eric Finster; Samuel Mimram (CoRR, 2021)

Monoidal weak omega-categories as models of a type theory. - Thibaut Benjamin (CoRR, 2021)

Formalization of dependent type theory: The example of CaTT. - Thibaut Benjamin (CoRR, 2021)

Formalizing an Efficient Runtime Assertion Checker for an Arithmetic Language with Functions and Predicates. - Thibaut Benjamin; Julien Signoles (SAC, 2023)

Abstract Interpretation of Recursive Logic Definitions for Efficient Runtime Assertion Checking. - Thibaut Benjamin; Julien Signoles (TAP, 2023)

Monoidal weak ω-categories as models of a type theory. - Thibaut Benjamin (Math. Struct. Comput. Sci., 2023)

Duality for weak ω-categories and the suspension and hom adjunction. - Thibaut Benjamin; Ioannis Markakis (CoRR, 2024)

CaTT contexts are finite computads. - Thibaut Benjamin; Ioannis Markakis; Chiara Sarti (CoRR, 2024)

Invertible cells in ω-categories. - Thibaut Benjamin; Ioannis Markakis (CoRR, 2024)

Generating Higher Identity Proofs in Homotopy Type Theory. - Thibaut Benjamin (CoRR, 2024)

Naturality for higher-dimensional path types. - Thibaut Benjamin; Ioannis Markakis; Wilfred Offord; Chiara Sarti; Jamie Vicary (CoRR, 2025)

Higher Eckmann-Hilton Arguments in Type Theory. - Thibaut Benjamin; Ioannis Markakis; Wilfred Offord; Chiara Sarti; Jamie Vicary (CoRR, 2025)

AdapTT: Functoriality for Dependent Type Casts. - Arthur Adjedj; Meven Lennon-Bertrand; Thibaut Benjamin; Kenji Maillard (CoRR, 2025)