Arthur Adjedj
Current Organizations / Institutes
The organizations/institutes from the scholar's latest article
Research Subjects
Research Interests
Arthur Adjedj has a total of 3 co-authors. Here are the top co-authors by number of shared publications:
- Kenji Maillard
Inria, Nantes, France
1 shared publication - Meven Lennon-Bertrand
University of Cambridge
1 shared publication - Thibaut Benjamin
Université Paris-Saclay - CNRS - ENS Paris-Saclay - LMF, Gif-sur-Yvette, France
1 shared publication
Latest Publications
- Open Access
- 8 January 2026
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 10 (POPL) , 628-658
AdapTT: Functoriality for Dependent Type Casts
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.
- 8 January 2026
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 10 (POPL) , 628-658
Open AccessAdapTT: Functoriality for Dependent Type Casts
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.