Thiago Felicissimo

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)

• Generic bidirectional typing for dependent type theories
  2024, Draft
  (subsumes the ESOP'24 paper)


• Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti
  with Théo Winterhalter
  2024, Submitted
  
  
• Generic bidirectional typing for dependent type theories
  2024, 33rd European Symposium on Programming (ESOP 2024)
  [artifact report] [technical report]


• Sharing proofs with predicative theories through universe polymorphic elaboration
  with Frédéric Blanqui
  2023, Submitted
  (subsumes the CSL'23 paper)


• A Confluence Criterion for Non Left-Linearity in a Beta/Eta-Free Reformulation of HRSs
  2023, 11th International Workshop on Higher-Order Rewriting
  [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
  


• 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]


• Adequate and Computational Encodings in the Logical Framework Dedukti
  2022, 7th International Conference on Formal Structures for Computation and Deduction
  [long version]


• 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, ESOP 2024, April 2024
• Generic bidirectional typing for dependent type theories, WG6 meeting, April 2024
• 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