Nicolas Tabareau
Inria Senior Researcher
Head of the Gallinette team

News

• Incremental Certified Programming T. Díaz, K. Maillard, É. Tanter, N. Tabareau. Accepted at OOPSLA'25, Singapour.
• Robust Dynamic Embedding for Gradual Typing K. Jacobs, M. Toro. N. Tabareau, É. Tanter. Accepted at ICFP'25, Singapour.
• I am the CPP'26 co-chair with Nik Swamy. It will be in Rennes, USA.
• All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants J. Poiret, G. Gilbert, K. Maillard, P. Pédrot, M. Sozeau, N. Tabareau, É. Tanter. Accepted at POPL'25, Denver, USA.
• Observational Equality meets CIC L. Pujet, Y. Leray, N. Tabareau. ACM TOPLAS, Volume 47, Issue 2 Article No.: 6, Pages 1 - 35 (extended version of ESOP'24).
• Correct and Complete Type Checking and Certified Erasure for Coq, in Coq M. Sozeau, Y. Forster, M. Lennon-Bertrand, J. Botsch Nielsen, N. Tabareau, T. Winterhalter. Journal of the ACM, Volume 72, Issue 1 (2025)
• Gradual Indexed Inductive Types M. Malewski, K. Maillard, N. Tabareau, E. Tanter. ICFP'24, Milan, Italy.
• The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant Y. Leray, G. Gilbert, N. Tabareau, T. Winterhalter. ITP'24, Tbilisi, Georgia.
• Verified Extraction from Coq to OCaml Y. Forster, M. Sozeau, N. Tabareau. PLDI'24, Copenhagen, Denmark (distinguished paper).

Current Projects

• GRAPA, Inria Associate Team (PI, 2023-2025).
• LiberAbaci Defi Inria (participant, 2022-2027).
• LLM4Code Defi Inria (participant, 2024-2029).

What I'm interested in

My research focuses on enhancing proof assistants by advancing the underlying theoretical framework. The results of this work include publications in leading international venues and the transfer of technology into mainstream proof assistants, particularly the Rocq Prover, which is primarily developed by my team at Inria.

Softwares

Here is a list of softwares/developments I have co-developed:

• Forcing for Coq - An extension of Coq that integrates forcing. It enables in particular to use general inductive types with Coq.
• Aspect JoCaml - A distributed aspect calculus based on JoCaml.
• Strid - A string diagram generator.

PhD Students

Here is a list of my past/current PhD students.

• Ismael Figueroa: Effective Aspects - A Typed Monadic Model to Control and Reason About Aspect. Defended in Lugano, 22-04-2014.
  Now: Assistant Professor at Universidad Católica de Valparaiso (Chile).
• Guilhem Jaber: A Logical Study of Program Equivalence. Defended at Institut Henri Poincaré, Paris, 11-07-2014.
  Now: Assitant Professor, Gallinette team, Univ Nantes.
• Kevin Quirin: Lawvere-Tierney sheafification in Type Theory. Defended in Nantes, 16-12-2016.
  Now: Professeur agrégé de mathémtiques en Lycée.
• Simon Boulier: Extending Type Theory with Syntactic Models. Defended in Nantes, 29-11-2018.
  Now: working on a biodynamic farming project.
• Gaëtan Gilbert: A type theory with definitional proof-irrelevance Defended in Nantes on December 2019.
  Now: Expert Engineer in the Rocq Consortium.
• Ambroise Lafont: Signatures and models for syntax and operational semantics in the presence of variable binding Defended in Nantes on December 2019.
  Now: Assistant professor at Ecole Polytechnique.
• Théo Winterhalter: Formalisation and meta-theory of type theory Defended in Nantes on September 2020
  Now: Inria Junior Researcher at Inria Saclay.
• Meven Lennon-Bertrand: Bidirectional Typing for the Calculus of Inductive Constructions Defended in Nantes on June 2022
  Now: Post-Doc in Cambridge, UK.
• Loïc Pujet: Computing with Extensionality Principles in Dependent Type Theory Defended in Nantes on December 2022
  Now: Sverker-Lerheden Fellow, University of Stockholm.
• Josselin Poiret: Started on 2023
• Yann Leray: Started on 2023
• Thomas Lamiaux: Started on 2024

Post-Docs

Here is a list of my past/current post-docs and engineers.

• Benedikt Ahrens: (2015-2017) Now assistant professor at Delft University of Technology, The Netherlands, and Birmingham Fellow.
• Pierre-Marie Pédrot: (2016-2018) Now Inria Research Scientist, Gallinette team, Nantes.
• Danil Annenkov: (2017-2018) Now Senior Scientist at Concordium.
• Pierre Vial: (2018-2019) Now Software Engineer at Formal Land.
• Maxime Lucas: (2018-2019) Now Software Engineer at SYSNAV.
• Simon Boulier: (2018-2019) Now working on a biodynamic farming project.
• Kenji Maillard (2020-2022): Now Inria Starting Faculty Position, Gallinette team, Nantes.
• Yannick Forster: (2021-2023) Marie Skłodowska-Curie fellow, Now Inria Research Scientist, Cambium team, Paris.
• Kazuhiko Sakaguchi: (2022-now) Working on correct extraction from Coq to Ocaml.
• Koen Jacobs: (2022-now) Working on gradual type systems.

Publications

• Type Theory:
  • Incremental Certified Programming T. Díaz, K. Maillard, É. Tanter, N. Tabareau. Accepted at OOPSLA'25, Singapour.
  • All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants J. Poiret, G. Gilbert, K. Maillard, P. Pédrot, M. Sozeau, N. Tabareau, É. Tanter. Accepted at POPL'25, Denver, USA.
  • Observational Equality meets CIC L. Pujet, Y. Leray, N. Tabareau. ACM TOPLAS, Volume 47, Issue 2 Article No.: 6, Pages 1 - 35 (extended version of ESOP'24).
  • Correct and Complete Type Checking and Certified Erasure for Coq, in Coq M. Sozeau, Y. Forster, M. Lennon-Bertrand, J. Botsch Nielsen, N. Tabareau, T. Winterhalter. Journal of the ACM, Volume 72, Issue 1 (2025)
  • Gradual Indexed Inductive Types M. Malewski, K. Maillard, N. Tabareau, E. Tanter. ICFP'24, Milan, Italy.
  • The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant Y. Leray, G. Gilbert, N. Tabareau, T. Winterhalter. ITP'24, Tbilisi, Georgia.
  • Verified Extraction from Coq to OCaml Y. Forster, M. Sozeau, N. Tabareau. PLDI'24, Copenhagen, Denmark.
  • Observational Equality meets CIC L. Pujet, N. Tabareau. ESOP'24, Luxembourg.
  • Impredicative Observational Equality L. Pujet, N. Tabareau. POPL'23, Boston, USA.
  • A Reasonably Gradual Type Theory K. Maillard, M. Lennon-Bertrand, N. Tabareau, É. Tanter. Accepted at ICFP'22.
  • Gradualizing the Calculus of Inductive Constructions. M. Lennon-Bertrand, K. Maillard, N. Tabareau, É. Tanter. To appear at TOPLAS (presented at POPL'22, Philadelphia, USA).
  • Observational Equality: Now For Good. L. Pujet, N. Tabareau. POPL'22, Philadelphia, USA.
  • The Taming of the Rew: A Type Theory with Computational Assumptions. J. Cockx, N. Tabareau, T. Winterhalter. POPL'21, Online.
  • The Marriage of Univalence and Parametricity. N.Tabareau., E. Tanter, M. Sozeau. Journal of the ACM 68, 1, Article 5 (February 2021), 44 pages.
  • Model structure on the universe of all types in interval type theory. S. Boulier, N. Tabareau. Mathematical Structures in Computer Science, Cambridge University Press, 2020.
  • The MetaCoq Project. M. Sozeau et al. Journal of Automated Reasoning, 64, pages 947–999 (2020).
  • The Fire Triangle: How to Mix Substitutions, Dependent Elimination and Effects. P.-M. Pédrot, N.Tabareau. POPL'20, New-Orleans, USA.
  • Coq Coq Correct: Verification of Type Checking and Erasure for Coq, in Coq. M. Sozeau, S. Boulier, Y. foster, N . Tabareau, T. Winterhalter. POPL'20, New-Orleans, USA.
  • A Reasonably Exceptional Type Theory. P.-M. Pédrot, N.Tabareau, H. Fehrmann, E. Tanter. ICFP'19, Berlin, Germany.
  • Setoid type theory --- a syntactic translation. T. Altenkirch, S. Boulier, A. Kaposi, N. Tabareau. MPC'19, Porto, Portugal.
  • Eliminating Reflection from Type Theory: In Memory of Martin Hofmann. T. Winterhalter, M. Sozeau, N. Tabareau. CPP'19, Cascais, Portugal.
  • Definitional Proof-Irrelevance without K. G. Gilbert, J. Cockxn, M. Sozeau, N. Tabareau. POPL'19.
  • Equivalences for Free! Univalent Parametricity for Effective Transport (distinguished paper award). N.Tabareau, E. Tanter, M. Sozeau. ICFP'18, Saint-Louis, USA.
  • Towards Certified Meta-Programming with Typed Template-Coq. A. Anand, S. Boulier, C. Cohen, M. Sozeau and N. Tabareau. Accepted at ITP'18, Okford, UK.
  • Failure is Not an Option. Pédrot P.-M., Tabareau N. Accepted at ESOP'18, Thessaloniki, Greece.
  • Foundations of Dependent Interoperability. Dagand P.-E., Tabareau N., Tanter E. Journal of Functional Programming, 28, E9 doi 2018. (journal version of our ICFP'16 paper).
  • Type-Theoretic Galois Connections. Dagand P.-E., Tabareau N., Tanter E. Principles of Secure Compilation (PriSC), 2018. A satellite workshop of POPL'18.
  • Typed Template Coq. Boulier, S, Sozeau M., Tabareau N., Anand, A. CoqPL, 2018. A satellite workshop of POPL'18.
  • An Effectful Way to Eliminate Addiction to Dependence. Pédrot P.-M., Tabareau N. LICS'17, Reykjavik, Iceland.
  • The next 700 syntactical models of type theory. Boulier S., Pédrot, P.-M. and Tabareau N. Accepted at CPP'17, Paris, France.
  • Lawvere-Tierney sheafification in Homotopy Type Theory. Quirin, K. and Tabareau N. Journal of Formalized Reasoning, 2016, 9 (2)
  • Partial Type Equivalences for Verified Dependent Interoperability Dagand P.-E., Tabareau N., Tanter E. Accepted at ICFP'16, Nara, Japan.
  • The Definitional Side of the Forcing. Jaber G., Lewertowski G., Pédrot P.-M., Sozeau M., Tabareau N. Accepted at LICS'16, NYC, USA.
  • Gradual Certified Programming in Coq Tanter, É., Tabareau N. DLS'15, Pittsburgh, USA.
  • Wild omega-Categories for the Homotopy Hypothesis in Type Theory Hirschowitz A., Hirschowitz T., Tabareau N. TLCA 2015, Warsaw, Poland.
  • Lost in Extraction, Recovered Tanter É., Tabareau N. ACM SIGPLAN ML Family Workshop, Vancouver, Canada, September 2015
  • Internalization of the Groupoid Interpretation of Type Theory. Sozeau M., Tabareau N. TYPES 2014, Paris, France. Coq development.
  • Universe Polymorphism in Coq. Sozeau M., Tabareau N. Interactive Theorem Proving (ITP) 2014, Vienna , Austria.
  • Extending Type Theory with Forcing. Jaber G., Sozeau M., Tabareau N. LICS 2012, Dubrovnik, Croatia. (technical appendix).
  • Decomposing Logical Relations with Forcing Jaber G. and Tabareau N. Draft
• Aspect Oriented Programming:
  • Chemical Foundations of Distributed Aspects. N.Tabareau, E. Tanter. Distributed Computing. June 2019, Volume 32, Issue 3, pp 193–216.
  • Compositional Reasoning About Aspect Interference Figuero I., Schrijvers T., Tabareau N., Tanter É. Modularity'14 (formerly AOSD), Lugano, Switzerland.
  • Aspectsual Session Types Tabareau N., Südholt M., Tanter É. Modularity'14 (formerly AOSD), Lugano, Switzerland.
  • Effective Aspects: A Typed Monadic Embedding of Pointcuts and Advice Figueroa I., Tabareau N., Tanter É. Transactions on Aspect-Oriented Software Development XI. LNCS Volume 8400, 2014, pp 145-192.
  • Execution Levels for Aspect-Oriented Programming Tanter É., Figueroa I., Tabareau N. Science of Computer Programming (SCP). Volume 80, Part B, 1 February 2014, Pages 311–342.
  • A Typed Monadic Embedding of Aspects Tabareau N., Figueroa I., Tanter É. AOSD'13 , Fukuoka, Japan.
  • Taming aspects with monads and membranes Figueroa I., Tabareau N., Tanter É. FOAL'13 , Fukuoka, Japan.
  • A monadic interpretation of execution levels and exceptions for AOP Tabareau N. AOSD'12 , Potsdam, Germany.
  • Taming aspects with membranes Tanter É., Tabareau N. and Douence R. Short version at FOAL'12 , Potsdam.
  • A Practical Monadic Aspect Weaver Figueroa I., Tanter É. and Tabareau N. FOAL'12 , Potsdam.
  • Exploring Membranes for Controlling Aspects Tanter E., Tabareau N. and Douence R. Techincal Report.
  • Aspect Oriented Programming: a language for 2-categories Tabareau N. FOAL'11.
  • A theory of distributed aspects Tabareau N. AOSD'10, Saint-Malo, France.
• Functional Programming:
  • Robust Dynamic Embedding for Gradual Typing K. Jacobs, M. Toro. N. Tabareau, É. Tanter. Accepted at ICFP'25, Singapour.
  • Kripke Open Bisimulation: A Marriage of Game Semantics and Operational Techniques. Jaber G., Tabareau N. APLAS'15, Pohang, Korea.
  • Lazier Imperative Programming Douence R., Tabareau N. Accepted at PPDP'14, Canterbury, UK.
  • Effect Capabilities in Haskell. Figueroa I., Tabareau N., Tanter E. Accepted at SBLP'14, Maceio, Brazil.
  • Effect Capabilities for Haskell: Taming Effect Interference in Monadic Programming. Figueroa I., Tabareau N., Tanter E. Accepted at SBLP'14, Maceio, Brazil. Science of Computer Programming (SCP). Journal version of the SBLP'14 paper.
  • Anti-unification with type classes. Tabareau N., Tanter E., Figueroa I. JFLA 2013, Aussois, France.
• Low level semantics:
  • Compiling Functional Types to Relational Specifications for Low Level Imperative Code Benton N., Tabareau N. TLDI 09. (you can find the Coq proofs here, it takes 10min to compile on a MacBook Pro with coq 8.2pl1)
  • Krivine realizability for compiler correctness Jaber G., Tabareau N. LOLA 2010, Edinburgh. A satellite workshop of LICS 2010. (you can find the Coq proofs here, it takes 3min to compile on a MacBook Pro with coq 8.2pl1)
  • The Journey of Biorthogonal Logical Relations to the Realm of Assembly Code Jaber G., Tabareau N. LOLA 2011, Toronto. A satellite workshop of LICS 2011.
• Linear Logic and Games semantics:
  • Master's thesis (in french)
  • Resource modalities in game semantics Melliès P.A., Tabareau N. Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, pages 389--398, 2007, IEEE Computer Society Washington, DC, USA.
  • Resource modalities in tensor logic Melliès P.A., Tabareau N. Annals of Pure and Applied Logic Volume 161, Issue 5, February 2010, Pages 632-653.
  • An algebraic account of references in game semantics Melliès P.A., Tabareau N. MFPS 2009
  • Linear continuations and duality Melliès P.A., Tabareau N. Unpublished
  • Free models of T-algebraic theories computed as Kan extensions Melliès P.A., Tabareau N. International Category Theory Conference, Calais 2008.
  • An explicit formula for the free exponential modality of linear logic. Melliès P.A., Tabareau N., Tasson C. ICALP 2009
  • An explicit formula for the free exponential modality of linear logic (journal version). Melliès P.A., Tabareau N., Tasson C. Mathematical Structure in Computer Science
  • Linear logic as a foundation for service-oriented computing Grall H., Tabareau N. Unpublished.
• Contraction and Brain:
  
  • Where neuroscience and dynamic system theory meet autonomous robotics: A contracting basal ganglia model for action selection. Girard B.,Tabareau N., Pham Q.-C., Berthoz A., Slotine J.-J. (2008) Neural Networks 21: 628-641
  • Geometry of the superior colliculus mapping and efficient oculomotor computation. Tabareau N., Bennequin D., Slotine J.-J., Berthoz A., Girard B. (2007) Biological Cybernetics 97(4): 279-292.
  • Contracting model of the basal ganglia. Girard B., Tabareau N., Slotine J.-J. and Berthoz A. In Bryson, J., Prescott, T. and Seth, A. (Eds) Modelling Natural Action Selection: Proceedings of an International Workshop, pages 69-76. AISB Press, Brighton, UK.
  • Selective amplification using a contracting model of the basal ganglia. Girard, B., Tabareau, N., Berthoz, A. and Slotine, J.-J. (2006). In Alexandre, F., Boniface, Y., Bougrain, L., Girau, B. and Rougier, N. (Eds) NeuroComp 2006, pages 30-33. [website]
  • Implementation of a neurophysiologic model of saccadic movements on an anthropomorphic robotic head. Manfredi, L., Maini, E., Laschi, C., Dario, P., Girard, B., Tabareau, N. and Berthoz, A. (2006). In IEEE-RAS Int. Conf. on Humanoid Robots, pages 438-443. [website]
• Stochastic contraction:
  
  • A Contraction Theory Approach to Stochastic Incremental Stability Pham Q.-C., Slotine J.-J. and Tabareau N. IEEE Transactions on Automatic Control, vol. 54, pp. 816-820, 2009
  • How synchronization protects from noise Tabareau N, Slotine J-J, Pham Q-C, 2010 PLoS Computational Biology 6(1)
• Timed Automata:
  
  • On timed automata with input-determined guards D'Souza D. and Tabareau N. Proceedings FORMATS-FTRTFT 2004, LNCS 3253, 2004

Awards

• Rosemont/Demassieux PhD thesis award in applied and fundamental mathematics from La Chancellerie des Universités de Paris, 2009
• Second Gilles Kahn PhD thesis award from the Société des Personnels Enseignants et Chercheurs en Informatique de France (specif), 2009