Nicolas Tabareau

Research

News

New Inria Associate Team GRAPA (Gradual Proof Assistants) funded for 2023-2025
Impredicative Observational Equality L. Pujet, N. Tabareau. POPL'23, Boston, USA.
PC member of POPL'23
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. Distinguished paper.
The EPIT School on Homotopy Type Theory has taken place online. April 12-16 2021. You can watch the videos of the lectures on the YouTube Channel of the school.
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.

Current Projects

CoqExtra (PI, 2020-2023), founded by Nomadic Labs.
ProverFX (PI, 2021-2022), Tremplin ANR.

What I'm interested in

Proof Assistant (Coq)
(Homotopy) Type Theory
Category theory
Semantics for low level languages
Cognitive Science
Aspect Oriented Programming

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.
Gabriel Lewertowski: Left for industry on Oct. 2016
Gaëtan Gilbert: A type theory with definitional proof-irrelevance Defended in Nantes on December 2019.
Now: Expert Engineer in the Coq Consortium.
Ambroise Lafont: Signatures and models for syntax and operational semantics in the presence of variable binding Defended in Nantes on December 2019.
Now: Post-doc in Cambridge, UK.
Théo Winterhalter: Formalisation and meta-theory of type theory Defended in Nantes on September 2020
Now: Inria Junior Researcher at Inria Saclay.
Meven Mertrand: 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: still on contract in the team.
Xavier Montillet: Started on Sept. 2017
Pierre Benjamin Giraud: Started on Jan. 2021

Post-Docs

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

Benedikt Ahrens: Now assistant professor at Delft University of Technology, The Netherlands.
Pierre-Marie Pédrot: Now Inria researcher, Gallinette team, Nantes.
Danil Annenkov: Now postdoc at Aarhus University.
Pierre Vial: Now post-doc at LRI, Paris.
Maxime Lucas: Now post-doc at LIPN (Paris Nord) with Thomas Seiller.
Simon Boulier: Now working on a biodynamic farming project.
Kenji Maillard: Now Inria Starting Faculty Position in the Gallinette team.
Kazuhiko Sakaguchi: Working a correct extraction from Coq to Ocaml.

Publications

Type Theory:
- 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 É., 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:
- 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

PhD thesis

"Modalités de ressource et contrôle en logique tensorielle", Université Denis Diderot - Paris VII (03/12/2008), Paul-André Melliès (Dir.)

Manuscript (in french)
Slides (in english)

HDR

The manuscrit of my HDR is available here

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

Nicolas Tabareau
Inria Senior Researcher
Head of the Gallinette team

Research

News

Current Projects

What I'm interested in

Softwares

PhD Students

Post-Docs

Publications

PhD thesis

HDR

Awards

Perso

Some useful links

Where to contact me

Nicolas Tabareau Inria Senior Researcher Head of the Gallinette team

Research

News

Current Projects

What I'm interested in

Softwares

PhD Students

Post-Docs

Publications

PhD thesis

HDR

Awards

Perso

Some useful links

Where to contact me

Nicolas Tabareau
Inria Senior Researcher
Head of the Gallinette team