Thiago Felicissimo
This website is no longer maintained, click here for my new website.
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
PhD Defense
On September 18th 2024 at 3 pm (CEST) I will defend my PhD thesis, entitled
Generic Bidirectional Typing in a Logical Framework for Dependent Type Theories
The defense will take place at the ENS Paris-Saclay (room 1Z18) and can also be attended online using this Zoom link.
The jury will be composed of Herman Geuvers (reviewer), Andrej Bauer (reviewer), Christine Paulin-Mohring, Frank Pfenning, Temur Kutsia, Marc Bezem, Frédéric Blanqui (supervisor) and Gilles Dowek (supervisor).
The current version of the manuscript can be found here.
Publications
Legend: ➺ (Journal), ✒ (Formal Proceedings), ✑ (Informal Proceedings), ✏ (Manuscript)
- Sharing proofs with predicative theories through universe-polymorphic elaboration
with Frédéric Blanqui
2024, Logical Methods in Computer Science (LMCS)
Subsumed by my PhD thesis
- Second-order Church-Rosser modulo, without normalization
2024, 13th International Workshop on Confluence (IWC 2024)
[technical report]
- Towards a logical framework modulo rewriting and equational theories
with Bruno Barras and Théo Winterhalter
2024, 30th International Conference on Types for Proofs and Programs (TYPES 2024)
- Generic bidirectional typing for dependent type theories
2024, Submitted
- Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti
with Théo Winterhalter
2024, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
[technical report]
- Generic bidirectional typing for dependent type theories
2024, 33rd European Symposium on Programming (ESOP 2024)
[artifact report] [technical report]
Subsumed by this draft and my PhD thesis
- A Confluence Criterion for Non Left-Linearity in a Beta/Eta-Free Reformulation of HRSs
2023, 11th International Workshop on Higher-Order Rewriting (HOR 2023)
[long version]
- A Logical Framework for Computational Type Theories with Erased Syntax and Bidirectional Typing
2023, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
- Translating Proofs from an Impredicative Type System to a Predicative One
with Frédéric Blanqui and Ashish Kumar Barnawal
2023, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
[long version]
Subsumed by the LMCS article and my PhD thesis
- Adequate and Computational Encodings in the Logical Framework Dedukti
2022, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
[long version]
Mostly subsumed by my PhD thesis
- No need to be implicit!
2022, Manuscript
- Cellular automata-based byte error correction in QCA
with Luiz FM Vieira, Marcos AM Vieira and Omar P Vilela Neto
2020, Nano Communication Networks
Talks
- Generic bidirectional typing for dependent type theories, Departamento de Ciência da Computação (DCC), August 2024
- Second-order Church-Rosser modulo, without normalization, IWC 2024, July 2024
- Generic bidirectional typing for dependent type theories, ESOP 2024, April 2024
- Generic bidirectional typing for dependent type theories, WG6 meeting, April 2024 [video]
- Generic bidirectional typing for dependent type theories, LMF Non-Permanent Members Seminar, November 2023
- Generic bidirectional typing for dependent type theories, Journées 2023 du GT Scalp, November 2023
- Generic bidirectional typing for dependent type theories, Formath Seminar at IRIF, October 2023
- Generic bidirectional typing for dependent type theories, SANDWICH Seminar at Computer Laboratory, September 2023
- A Logical Framework for Computational Type Theories with Erased Syntax and Bidirectional Typing, Departamento de Informática at PUC-Rio, August 2023
- 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, AIST, 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