I am a PhD student since October 2021 under the supervision of Frédéric Blanqui and Gilles Dowek at Deducteam, an Inria research team at Laboratoire Méthodes Formelles (LMF).
I am interested in logical frameworks, type theory, proof assistants and rewriting.
- Email: thiago (dot) felicissimo (at) inria (dot) fr
- Address: Office 3S63, ENS Paris-Saclay
- GitHub: thiagofelicissimo
Publications
Legend: ➺ (Journal), ✒ (Formal Proceedings), ✑ (Informal Proceedings), ✏ (Manuscript)
Talks
- A Logical Framework for Computational Type Theories with Erased Syntax and Bidirectional Typing, TYPES 2023, June 2023
- A Logical Framework for Computational Type Theories with Minimal Syntax and Bidirectional Typing, WG6 meeting, April 2023
- Translating proofs from an impredicative type system to a predicative one, CSL 2023, February 2023
- Translating proofs from an impredicative type system to a predicative one, Deducteam Seminar, January 2023
- Translating proofs from an impredicative type system to a predicative one, Kiryu, November 2022
- Translating proofs from an impredicative type system to a predicative one, Tokyo, November 2022
- Adequate and computational encodings in the logical framework Dedukti, FSCD 2022, August 2022
- Adequate and computational encodings in the logical framework Dedukti, Deducteam's Interns Day 2022, July 2022
- How to write a translator to Dedukti? The case of Agda, with Jesper Cockx at the 1st Dedukti School, June 2022 [video]
- A framework for defining type theories, Programming Languages Seminar at TU Delft's PL Group, May 2022
- A framework for defining type theories, participant talk at MGS 2022, April 2022
Teaching
2022-2023
- TD Logique pour l'informatique, with Christine Paulin-Mohring, L3 Faculté des Sciences d'Orsay
- TP Programmation Fonctionnelle, with Pablo Arrighi, Polytech Paris-Saclay
- TD/TP Compilation, with Thibaut Balabonski, L3 Faculté des Sciences d'Orsay
2021-2022
- TD Logique pour l'informatique, with Christine Paulin-Mohring, L3 Faculté des Sciences d'Orsay
- TP Programmation Fonctionnelle Avancée, with Pablo Arrighi, L3 Faculté des Sciences d'Orsay
- TP Développement Orienté Objets, with Jean-Claude Martin, IUT d'Orsay