Adequate and Computational Encodings in the Logical Framework Dedukti. - Thiago Felicissimo (FSCD, 2022)

Translating Proofs from an Impredicative Type System to a Predicative One. - Thiago Felicissimo; Frédéric Blanqui; Ashish Kumar Barnawal (CSL, 2023)

A framework for erased syntax and bidirectional typing. - Thiago Felicissimo (CoRR, 2023)

Artifact report: Generic bidirectional typing for dependent type theories. - Thiago Felicissimo (ESOP (1), 2024)

Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. - Thiago Felicissimo; Théo Winterhalter (FSCD, 2024)

Sharing proofs with predicative theories through universe-polymorphic elaboration. - Thiago Felicissimo; Frédéric Blanqui (Log. Methods Comput. Sci., 2024)

Generic bidirectional typing in a logical framework for dependent type theories. (Typage bidirectionnel générique dans un logical framework pour les théories des types dépendants). - Thiago Felicissimo (2024)

Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting. - Thiago Felicissimo; Jean-Pierre Jouannaud (CADE, 2025)

Generic Bidirectional Typing for Dependent Type Theories. - Thiago Felicissimo (ACM Trans. Program. Lang. Syst., 2025)