Nicolas Tabareau

ORCID

Publication Activity (10 Years)

Years Active: 2004-2024
Publications (10 Years): 37

Top Venues

Proc. ACM Program. Lang.

CoRR

ITP

Math. Struct. Comput. Sci.

Paris Diderot University, France (PHD)

Education History

Paris Diderot University, France

PHD

Publications

Yannick Forster, Matthieu Sozeau, Nicolas Tabareau
Verified Extraction from Coq to OCaml. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Loïc Pujet, Nicolas Tabareau
Observational Equality Meets CIC. ESOP (1) (2024)
Loïc Pujet, Nicolas Tabareau
Impredicative Observational Equality. Proc. ACM Program. Lang. 7 (POPL) (2023)
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter
A reasonably gradual type theory. Proc. ACM Program. Lang. 6 (ICFP) (2022)
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter
A Reasonably Gradual Type Theory. CoRR (2022)
Loïc Pujet, Nicolas Tabareau
Observational equality: now for good. Proc. ACM Program. Lang. 6 (POPL) (2022)
Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter
Gradualizing the Calculus of Inductive Constructions. ACM Trans. Program. Lang. Syst. 44 (2) (2022)
Simon Boulier, Nicolas Tabareau
Model structure on the universe of all types in interval type theory. Math. Struct. Comput. Sci. 31 (4) (2021)
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
The Marriage of Univalence and Parametricity. J. ACM 68 (1) (2021)
Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter
The Multiverse: Logical Modularity for Proof Assistants. CoRR (2021)
Jesper Cockx, Nicolas Tabareau, Théo Winterhalter
The taming of the rew: a type theory with computational assumptions. Proc. ACM Program. Lang. 5 (POPL) (2021)
Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter
Gradualizing the Calculus of Inductive Constructions. CoRR (2020)
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
The MetaCoq Project. J. Autom. Reason. 64 (5) (2020)
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter
Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proc. ACM Program. Lang. 4 (POPL) (2020)
Pierre-Marie Pédrot, Nicolas Tabareau
The fire triangle: how to mix substitution, dependent elimination, and effects. Proc. ACM Program. Lang. 4 (POPL) (2020)
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
The Marriage of Univalence and Parametricity. CoRR (2019)
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau
Definitional proof-irrelevance without K. Proc. ACM Program. Lang. 3 (POPL) (2019)
Pierre-Marie Pédrot, Nicolas Tabareau, Hans Jacob Fehrmann, Éric Tanter
A reasonably exceptional type theory. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau
Eliminating reflection from type theory. CPP (2019)
Peter LeFanu Lumsdaine, Nicolas Tabareau
Preface: Special Issue on Homotopy Type Theory and Univalent Foundations. J. Autom. Reason. 63 (2) (2019)
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau
Setoid Type Theory - A Syntactic Translation. MPC (2019)
Nicolas Tabareau, Éric Tanter
Chemical foundations of distributed aspects. Distributed Comput. 32 (3) (2019)
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
Equivalences for free: univalent parametricity for effective transport. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau
Towards Certified Meta-Programming with Typed Template-Coq. ITP (2018)
Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter
Foundations of dependent interoperability. J. Funct. Program. 28 (2018)
Paul-André Melliès, Nicolas Tabareau, Christine Tasson
An explicit formula for the free exponential modality of linear logic. Math. Struct. Comput. Sci. 28 (7) (2018)
Pierre-Marie Pédrot, Nicolas Tabareau
Failure is Not an Option - An Exceptional Type Theory. ESOP (2018)
Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau
The next 700 syntactical models of type theory. CPP (2017)
Pierre-Marie Pédrot, Nicolas Tabareau
An effectful way to eliminate addiction to dependence. LICS (2017)
Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau
The Definitional Side of the Forcing. LICS (2016)
Ismael Figueroa, Nicolas Tabareau, Éric Tanter
Effect capabilities for Haskell: Taming effect interference in monadic programming. Sci. Comput. Program. 119 (2016)
Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter
Partial type equivalences for verified dependent interoperability. ICFP (2016)
Kevin Quirin, Nicolas Tabareau
Lawvere-Tierney sheafification in Homotopy Type Theory. J. Formaliz. Reason. 9 (2) (2016)
Éric Tanter, Nicolas Tabareau
Gradual certified programming in Coq. DLS (2015)
André Hirschowitz, Tom Hirschowitz, Nicolas Tabareau
Wild omega-Categories for the Homotopy Hypothesis in Type Theory. TLCA (2015)
Guilhem Jaber, Nicolas Tabareau
Kripke Open Bisimulation - A Marriage of Game Semantics and Operational Techniques. APLAS (2015)
Éric Tanter, Nicolas Tabareau
Gradual Certified Programming in Coq. CoRR (2015)
Éric Tanter, Ismael Figueroa, Nicolas Tabareau
Execution levels for aspect-oriented programming: Design, semantics, implementations and applications. Sci. Comput. Program. 80 (2014)
Ismael Figueroa, Tom Schrijvers, Nicolas Tabareau, Éric Tanter
Compositional reasoning about aspect interference. MODULARITY (2014)
Matthieu Sozeau, Nicolas Tabareau
Universe Polymorphism in Coq. ITP (2014)
Nicolas Tabareau, Mario Südholt, Éric Tanter
Aspectual session types. MODULARITY (2014)
Rémi Douence, Nicolas Tabareau
Lazier Imperative Programming. PPDP (2014)
Ismael Figueroa, Nicolas Tabareau, Éric Tanter
Effect Capabilities for Haskell. SBLP (2014)
Ismael Figueroa, Nicolas Tabareau, Éric Tanter
Effective Aspects: A Typed Monadic Embedding of Pointcuts and Advice. LNCS Trans. Aspect Oriented Softw. Dev. 11 (2013)
Ismael Figueroa, Nicolas Tabareau, Éric Tanter
Taming aspects with monads and membranes. FOAL (2013)
Nicolas Tabareau, Ismael Figueroa, Éric Tanter
A typed monadic embedding of aspects. AOSD (2013)
Éric Tanter, Nicolas Tabareau, Rémi Douence
Taming aspects with membranes. FOAL (2012)
Guilhem Jaber, Nicolas Tabareau, Matthieu Sozeau
Extending Type Theory with Forcing. LICS (2012)
Nicolas Tabareau
A monadic interpretation of execution levels and exceptions for AOP. AOSD (2012)
Ismael Figueroa, Éric Tanter, Nicolas Tabareau
A practical monadic aspect weaver. FOAL (2012)
Nicolas Tabareau
Aspect oriented programming: a language for 2-categories. FOAL (2011)
Nicolas Tabareau
A theory of distributed aspects. AOSD (2010)
Paul-André Melliès, Nicolas Tabareau
Resource modalities in tensor logic. Ann. Pure Appl. Log. 161 (5) (2010)
Nicolas Tabareau, Jean-Jacques E. Slotine, Quang-Cuong Pham
How Synchronization Protects from Noise. PLoS Comput. Biol. 6 (1) (2010)
Nick Benton, Nicolas Tabareau
Compiling functional types to relational specifications for low level imperative code. TLDI (2009)
Quang-Cuong Pham, Nicolas Tabareau, Jean-Jacques E. Slotine
A Contraction Theory Approach to Stochastic Incremental Stability. IEEE Trans. Autom. Control. 54 (4) (2009)
Paul-André Melliès, Nicolas Tabareau, Christine Tasson
An Explicit Formula for the Free Exponential Modality of Linear Logic. ICALP (2) (2009)
Paul-André Melliès, Nicolas Tabareau
An Algebraic Account of References in Game Semantics. MFPS (2009)
Benoît Girard, Nicolas Tabareau, Quang-Cuong Pham, Alain Berthoz, Jean-Jacques E. Slotine
Where neuroscience and dynamic system theory meet autonomous robotics: A contracting basal ganglia model for action selection. Neural Networks 21 (4) (2008)
Nicolas Tabareau, Daniel Bennequin, Alain Berthoz, Jean-Jacques E. Slotine, Benoît Girard
Geometry of the superior colliculus mapping and efficient oculomotor computation. Biol. Cybern. 97 (4) (2007)
Paul-André Melliès, Nicolas Tabareau
Resource modalities in game semantics. LICS (2007)
Paul-André Melliès, Nicolas Tabareau
Resource modalities in game semantics CoRR (2007)
Deepak D'Souza, Nicolas Tabareau
On timed automata with input-determined guards CoRR (2006)
Luigi Manfredi, Eliseo Stefano Maini, Paolo Dario, Cecilia Laschi, Benoît Girard, Nicolas Tabareau, Alain Berthoz
Implementation of a neurophysiological model of saccadic eye movements on an anthropomorphic robotic head. Humanoids (2006)
Nicolas Tabareau
De l'oprateur de trace dans les jeux de Conway CoRR (2006)
Deepak D'Souza, Nicolas Tabareau
On Timed Automata with Input-Determined Guards. FORMATS/FTRTFT (2004)

Nicolas Tabareau.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Nicolas Tabareau