On Timed Automata with Input-Determined Guards. - Deepak D'Souza; Nicolas Tabareau (FORMATS/FTRTFT, 2004)

Implementation of a neurophysiological model of saccadic eye movements on an anthropomorphic robotic head. - Luigi Manfredi; Eliseo Stefano Maini; Paolo Dario; Cecilia Laschi; Benoît Girard 001; Nicolas Tabareau; Alain Berthoz (Humanoids, 2006)

De l'oprateur de trace dans les jeux de Conway - Nicolas Tabareau (CoRR, 2006)

Resource modalities in game semantics. - Paul-André Melliès; Nicolas Tabareau (LICS, 2007)

Geometry of the superior colliculus mapping and efficient oculomotor computation. - Nicolas Tabareau; Daniel Bennequin; Alain Berthoz; Jean-Jacques E. Slotine; Benoît Girard 001 (Biol. Cybern., 2007)

Where neuroscience and dynamic system theory meet autonomous robotics: A contracting basal ganglia model for action selection. - Benoît Girard 001; Nicolas Tabareau; Quang-Cuong Pham; Alain Berthoz; Jean-Jacques E. Slotine (Neural Networks, 2008)

Modalités de ressource et contrôle en logique tensorielle. (Resource modalities and control in tensorial logic). - Nicolas Tabareau (2008)

Compiling functional types to relational specifications for low level imperative code. - Nick Benton; Nicolas Tabareau (TLDI, 2009)

An Algebraic Account of References in Game Semantics. - Paul-André Melliès; Nicolas Tabareau (MFPS, 2009)

A Contraction Theory Approach to Stochastic Incremental Stability. - Quang-Cuong Pham; Nicolas Tabareau; Jean-Jacques E. Slotine (IEEE Trans. Autom. Control., 2009)

A theory of distributed aspects. - Nicolas Tabareau (AOSD, 2010)

Resource modalities in tensor logic. - Paul-André Melliès; Nicolas Tabareau (Ann. Pure Appl. Log., 2010)

How Synchronization Protects from Noise. - Nicolas Tabareau; Jean-Jacques E. Slotine; Quang-Cuong Pham (PLoS Comput. Biol., 2010)

Aspect oriented programming: a language for 2-categories. - Nicolas Tabareau (FOAL, 2011)

A monadic interpretation of execution levels and exceptions for AOP. - Nicolas Tabareau (AOSD, 2012)

A practical monadic aspect weaver. - Ismael Figueroa; Éric Tanter; Nicolas Tabareau (FOAL, 2012)

Taming aspects with membranes. - Éric Tanter; Nicolas Tabareau; Rémi Douence (FOAL, 2012)

Extending Type Theory with Forcing. - Guilhem Jaber; Nicolas Tabareau; Matthieu Sozeau (LICS, 2012)

A typed monadic embedding of aspects. - Nicolas Tabareau; Ismael Figueroa; Éric Tanter (AOSD, 2013)

Taming aspects with monads and membranes. - Ismael Figueroa; Nicolas Tabareau; Éric Tanter (FOAL, 2013)

Effective Aspects: A Typed Monadic Embedding of Pointcuts and Advice. - Ismael Figueroa; Nicolas Tabareau; Éric Tanter (LNCS Trans. Aspect Oriented Softw. Dev., 2013)

Compositional reasoning about aspect interference. - Ismael Figueroa; Tom Schrijvers; Nicolas Tabareau; Éric Tanter (MODULARITY, 2014)

Aspectual session types. - Nicolas Tabareau; Mario Südholt; Éric Tanter (MODULARITY, 2014)

Universe Polymorphism in Coq. - Matthieu Sozeau; Nicolas Tabareau (ITP, 2014)

Lazier Imperative Programming. - Rémi Douence; Nicolas Tabareau (PPDP, 2014)

Effect Capabilities for Haskell. - Ismael Figueroa; Nicolas Tabareau; Éric Tanter (SBLP, 2014)

Execution levels for aspect-oriented programming: Design, semantics, implementations and applications. - Éric Tanter; Ismael Figueroa; Nicolas Tabareau (Sci. Comput. Program., 2014)

Kripke Open Bisimulation - A Marriage of Game Semantics and Operational Techniques. - Guilhem Jaber; Nicolas Tabareau (APLAS, 2015)

Gradual certified programming in Coq. - Éric Tanter; Nicolas Tabareau (DLS, 2015)

Wild omega-Categories for the Homotopy Hypothesis in Type Theory. - André Hirschowitz; Tom Hirschowitz; Nicolas Tabareau (TLCA, 2015)

Partial type equivalences for verified dependent interoperability. - Pierre-Évariste Dagand; Nicolas Tabareau; Éric Tanter (ICFP, 2016)

The Definitional Side of the Forcing. - Guilhem Jaber; Gabriel Lewertowski; Pierre-Marie Pédrot; Matthieu Sozeau; Nicolas Tabareau (LICS, 2016)

Lawvere-Tierney sheafification in Homotopy Type Theory. - Kevin Quirin; Nicolas Tabareau (J. Formaliz. Reason., 2016)

Effect capabilities for Haskell: Taming effect interference in monadic programming. - Ismael Figueroa; Nicolas Tabareau; Éric Tanter (Sci. Comput. Program., 2016)

The next 700 syntactical models of type theory. - Simon Boulier; Pierre-Marie Pédrot; Nicolas Tabareau (CPP, 2017)

An effectful way to eliminate addiction to dependence. - Pierre-Marie Pédrot; Nicolas Tabareau (LICS, 2017)

Failure is Not an Option - An Exceptional Type Theory. - Pierre-Marie Pédrot; Nicolas Tabareau (ESOP, 2018)

Towards Certified Meta-Programming with Typed Template-Coq. - Abhishek Anand; Simon Boulier; Cyril Cohen; Matthieu Sozeau; Nicolas Tabareau (ITP, 2018)

Foundations of dependent interoperability. - Pierre-Évariste Dagand; Nicolas Tabareau; Éric Tanter (J. Funct. Program., 2018)

An explicit formula for the free exponential modality of linear logic. - Paul-André Melliès; Nicolas Tabareau; Christine Tasson (Math. Struct. Comput. Sci., 2018)

Equivalences for free: univalent parametricity for effective transport. - Nicolas Tabareau; Éric Tanter; Matthieu Sozeau (Proc. ACM Program. Lang., 2018)

Eliminating reflection from type theory. - Théo Winterhalter; Matthieu Sozeau; Nicolas Tabareau (CPP, 2019)

Setoid Type Theory - A Syntactic Translation. - Thorsten Altenkirch; Simon Boulier; Ambrus Kaposi; Nicolas Tabareau (MPC, 2019)

Chemical foundations of distributed aspects. - Nicolas Tabareau; Éric Tanter (Distributed Comput., 2019)

Preface: Special Issue on Homotopy Type Theory and Univalent Foundations. - Peter LeFanu Lumsdaine; Nicolas Tabareau (J. Autom. Reason., 2019)

Definitional proof-irrelevance without K. - Gaëtan Gilbert; Jesper Cockx; Matthieu Sozeau; Nicolas Tabareau (Proc. ACM Program. Lang., 2019)

A reasonably exceptional type theory. - Pierre-Marie Pédrot; Nicolas Tabareau; Hans Jacob Fehrmann; Éric Tanter (Proc. ACM Program. Lang., 2019)

The MetaCoq Project. - Matthieu Sozeau; Abhishek Anand; Simon Boulier; Cyril Cohen; Yannick Forster 002; Fabian Kunze; Gregory Malecha; Nicolas Tabareau; Théo Winterhalter (J. Autom. Reason., 2020)

The fire triangle: how to mix substitution, dependent elimination, and effects. - Pierre-Marie Pédrot; Nicolas Tabareau (Proc. ACM Program. Lang., 2020)

Coq Coq correct! verification of type checking and erasure for Coq, in Coq. - Matthieu Sozeau; Simon Boulier; Yannick Forster 002; Nicolas Tabareau; Théo Winterhalter (Proc. ACM Program. Lang., 2020)

The Multiverse: Logical Modularity for Proof Assistants. - Kenji Maillard; Nicolas Margulies; Matthieu Sozeau; Nicolas Tabareau; Éric Tanter (CoRR, 2021)

The Marriage of Univalence and Parametricity. - Nicolas Tabareau; Éric Tanter; Matthieu Sozeau (J. ACM, 2021)

Model structure on the universe of all types in interval type theory. - Simon Boulier; Nicolas Tabareau (Math. Struct. Comput. Sci., 2021)

The taming of the rew: a type theory with computational assumptions. - Jesper Cockx; Nicolas Tabareau; Théo Winterhalter (Proc. ACM Program. Lang., 2021)

A reasonably gradual type theory. - Kenji Maillard; Meven Lennon-Bertrand; Nicolas Tabareau; Éric Tanter (Proc. ACM Program. Lang., 2022)

Observational equality: now for good. - Loïc Pujet; Nicolas Tabareau (Proc. ACM Program. Lang., 2022)

Gradualizing the Calculus of Inductive Constructions. - Meven Lennon-Bertrand; Kenji Maillard; Nicolas Tabareau; Éric Tanter (ACM Trans. Program. Lang. Syst., 2022)

Impredicative Observational Equality. - Loïc Pujet; Nicolas Tabareau (Proc. ACM Program. Lang., 2023)

Observational Equality Meets CIC. - Loïc Pujet; Nicolas Tabareau (ESOP (1), 2024)

The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. - Yann Leray; Gaëtan Gilbert; Nicolas Tabareau; Théo Winterhalter (ITP, 2024)

Verified Extraction from Coq to OCaml. - Yannick Forster 002; Matthieu Sozeau; Nicolas Tabareau (Proc. ACM Program. Lang., 2024)

Gradual Indexed Inductive Types. - Mara Malewski; Kenji Maillard; Nicolas Tabareau; Éric Tanter (Proc. ACM Program. Lang., 2024)

All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants. - Josselin Poiret; Gaëtan Gilbert; Kenji Maillard; Pierre-Marie Pédrot; Matthieu Sozeau; Nicolas Tabareau; Éric Tanter (Proc. ACM Program. Lang., 2025)

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. - Matthieu Sozeau; Yannick Forster 002; Meven Lennon-Bertrand; Jakob Botsch Nielsen; Nicolas Tabareau; Théo Winterhalter (J. ACM, 2025)

Observational Equality Meets CIC. - Loïc Pujet; Yann Leray; Nicolas Tabareau (ACM Trans. Program. Lang. Syst., 2025)