I am a postdoctoral researcher since October 2024 at Gallinette, an Inria research team at Laboratoire des sciences du numérique de Nantes (LS2N), working with Nicolas Tabareau.
Previously, from October 2021 to September 2024, I was a PhD student under the supervision of Frédéric Blanqui and Gilles Dowek at Deducteam, an Inria research team at Laboratoire Méthodes Formelles (LMF). More information about my PhD can be found here.
I am interested in logical frameworks, dependent type theory, proof assistants and rewriting.
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
PhD Thesis
On September 18th 2024 I defended my PhD thesis, entitled
Generic Bidirectional Typing in a Logical Framework for Dependent Type Theories
The thesis can be found here, and a recording of the presentation is available here.
The jury was composed of:
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