Effects and Modal Types.- Scoped Effects as Parameterized Algebraic Theories.- Intersection Types, Relationally.- Modal Type Theory: Where Meta-programming Meets Intentional Analysis.- Program Synthesis from Graded Types.- Bidirectional Typing and Session Types.- A Formal Treatment of Bidirectional Typing.- Generic bidirectional typing for dependent type theories.
- Artifact report: Generic bidirectional typing for dependent type theories.- Deciding Subtyping for Asynchronous Multiparty Sessions.- The Session Abstract Machine.- Dependent Types.- Trocq: Proof Transfer for Free, With or Without Univalence.- Artifact report: Trocq: Proof Transfer for Free, With or Without Univalence.- Observational Equality Meets CIC.- Definitional Functoriality for Dependent (Sub)Types.
- Artifact report: Definitional Functoriality for Dependent (Sub)Types.