Nicolas Tabareau

78 papers A* 4A 2B 10C 2Journal 43Unranked 16

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Bounded Sort Polymorphism with Elimination Constraints. Proc. ACM Program. Lang. Johann Rosain, Tomás Díaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, Théo Winterhalter
2026	B	`ed.`	Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2026, Rennes, France, January 12-13, 2026 CPP Kathrin Stark, Yannick Zakowski, Nikhil Swamy, Nicolas Tabareau
2026	J	`jnl`	The Rewster: Type Preserving Rewrite Rules for the Rocq Prover. J. Autom. Reason. Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter
2025	J	`jnl`	All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants. Proc. ACM Program. Lang. Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter
2025	J	`jnl`	Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. J. ACM Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter
2025	J	`jnl`	Incremental Certified Programming. Proc. ACM Program. Lang. Tomás Díaz, Kenji Maillard, Nicolas Tabareau, Éric Tanter
2025	J	`jnl`	Observational Equality Meets CIC. ACM Trans. Program. Lang. Syst. Loïc Pujet, Yann Leray, Nicolas Tabareau
2025	B	`ed.`	Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, Denver, CO, USA, January 20-21, 2025 CPP Kathrin Stark, Amin Timany, Sandrine Blazy, Nicolas Tabareau
2025	J	`jnl`	Robust Dynamic Embedding for Gradual Typing. Proc. ACM Program. Lang. Koen Jacobs, Matías Toro, Nicolas Tabareau, Éric Tanter
2024	J	`jnl`	Gradual Indexed Inductive Types. Proc. ACM Program. Lang. Mara Malewski, Kenji Maillard, Nicolas Tabareau, Éric Tanter
2024	—	`conf`	Observational Equality Meets CIC. ESOP (1) Loïc Pujet, Nicolas Tabareau
2024	B	`conf`	The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. ITP Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter
2024	J	`jnl`	Verified Extraction from Coq to OCaml. Proc. ACM Program. Lang. Yannick Forster, Matthieu Sozeau, Nicolas Tabareau
2023	J	`jnl`	Impredicative Observational Equality. Proc. ACM Program. Lang. Loïc Pujet, Nicolas Tabareau
2022	J	`jnl`	A Reasonably Gradual Type Theory. CoRR Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter
2022	J	`jnl`	A reasonably gradual type theory. Proc. ACM Program. Lang. Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter
2022	J	`jnl`	Gradualizing the Calculus of Inductive Constructions. ACM Trans. Program. Lang. Syst. Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter
2022	J	`jnl`	Observational equality: now for good. Proc. ACM Program. Lang. Loïc Pujet, Nicolas Tabareau
2021	J	`jnl`	Model structure on the universe of all types in interval type theory. Math. Struct. Comput. Sci. Simon Boulier, Nicolas Tabareau
2021	J	`jnl`	The Marriage of Univalence and Parametricity. J. ACM Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
2021	J	`jnl`	The Multiverse: Logical Modularity for Proof Assistants. CoRR Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter
2021	J	`jnl`	The taming of the rew: a type theory with computational assumptions. Proc. ACM Program. Lang. Jesper Cockx, Nicolas Tabareau, Théo Winterhalter
2020	J	`jnl`	Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proc. ACM Program. Lang. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter
2020	J	`jnl`	Gradualizing the Calculus of Inductive Constructions. CoRR Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter
2020	J	`jnl`	The MetaCoq Project. J. Autom. Reason. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
2020	J	`jnl`	The fire triangle: how to mix substitution, dependent elimination, and effects. Proc. ACM Program. Lang. Pierre-Marie Pédrot, Nicolas Tabareau
2019	J	`jnl`	A reasonably exceptional type theory. Proc. ACM Program. Lang. Pierre-Marie Pédrot, Nicolas Tabareau, Hans Jacob Fehrmann, Éric Tanter
2019	J	`jnl`	Chemical foundations of distributed aspects. Distributed Comput. Nicolas Tabareau, Éric Tanter
2019	J	`jnl`	Definitional proof-irrelevance without K. Proc. ACM Program. Lang. Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau
2019	B	`conf`	Eliminating reflection from type theory. CPP Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau
2019	J	`jnl`	Preface: Special Issue on Homotopy Type Theory and Univalent Foundations. J. Autom. Reason. Peter LeFanu Lumsdaine, Nicolas Tabareau
2019	B	`conf`	Setoid Type Theory - A Syntactic Translation. MPC Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau
2019	J	`jnl`	The Marriage of Univalence and Parametricity. CoRR Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
2018	J	`jnl`	An explicit formula for the free exponential modality of linear logic. Math. Struct. Comput. Sci. Paul-André Melliès, Nicolas Tabareau, Christine Tasson
2018	J	`jnl`	Equivalences for free: univalent parametricity for effective transport. Proc. ACM Program. Lang. Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
2018	A	`conf`	Failure is Not an Option - An Exceptional Type Theory. ESOP Pierre-Marie Pédrot, Nicolas Tabareau
2018	J	`jnl`	Foundations of dependent interoperability. J. Funct. Program. Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter
2018	B	`conf`	Towards Certified Meta-Programming with Typed Template-Coq. ITP Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau
2017	A*	`conf`	An effectful way to eliminate addiction to dependence. LICS Pierre-Marie Pédrot, Nicolas Tabareau
2017	B	`conf`	The next 700 syntactical models of type theory. CPP Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau
2016	J	`jnl`	Effect capabilities for Haskell: Taming effect interference in monadic programming. Sci. Comput. Program. Ismael Figueroa, Nicolas Tabareau, Éric Tanter
2016	J	`jnl`	Lawvere-Tierney sheafification in Homotopy Type Theory. J. Formaliz. Reason. Kevin Quirin, Nicolas Tabareau
2016	A	`conf`	Partial type equivalences for verified dependent interoperability. ICFP Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter
2016	A*	`conf`	The Definitional Side of the Forcing. LICS Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau
2015	J	`jnl`	Gradual Certified Programming in Coq. CoRR Éric Tanter, Nicolas Tabareau
2015	C	`conf`	Gradual certified programming in Coq. DLS Éric Tanter, Nicolas Tabareau
2015	B	`conf`	Kripke Open Bisimulation - A Marriage of Game Semantics and Operational Techniques. APLAS Guilhem Jaber, Nicolas Tabareau
2015	—	`conf`	Wild omega-Categories for the Homotopy Hypothesis in Type Theory. TLCA André Hirschowitz, Tom Hirschowitz, Nicolas Tabareau
2014	—	`conf`	Aspectual session types. MODULARITY Nicolas Tabareau, Mario Südholt, Éric Tanter
2014	—	`conf`	Compositional reasoning about aspect interference. MODULARITY Ismael Figueroa, Tom Schrijvers, Nicolas Tabareau, Éric Tanter
2014	—	`conf`	Effect Capabilities for Haskell. SBLP Ismael Figueroa, Nicolas Tabareau, Éric Tanter
2014	J	`jnl`	Execution levels for aspect-oriented programming: Design, semantics, implementations and applications. Sci. Comput. Program. Éric Tanter, Ismael Figueroa, Nicolas Tabareau
2014	C	`conf`	Lazier Imperative Programming. PPDP Rémi Douence, Nicolas Tabareau
2014	B	`conf`	Universe Polymorphism in Coq. ITP Matthieu Sozeau, Nicolas Tabareau
2013	—	`conf`	A typed monadic embedding of aspects. AOSD Nicolas Tabareau, Ismael Figueroa, Éric Tanter
2013	J	`jnl`	Effective Aspects: A Typed Monadic Embedding of Pointcuts and Advice. LNCS Trans. Aspect Oriented Softw. Dev. Ismael Figueroa, Nicolas Tabareau, Éric Tanter
2013	—	`conf`	Taming aspects with monads and membranes. FOAL Ismael Figueroa, Nicolas Tabareau, Éric Tanter
2012	—	`conf`	A monadic interpretation of execution levels and exceptions for AOP. AOSD Nicolas Tabareau
2012	—	`conf`	A practical monadic aspect weaver. FOAL Ismael Figueroa, Éric Tanter, Nicolas Tabareau
2012	A*	`conf`	Extending Type Theory with Forcing. LICS Guilhem Jaber, Nicolas Tabareau, Matthieu Sozeau
2012	—	`conf`	Taming aspects with membranes. FOAL Éric Tanter, Nicolas Tabareau, Rémi Douence
2011	—	`conf`	Aspect oriented programming: a language for 2-categories. FOAL Nicolas Tabareau
2010	—	`conf`	A theory of distributed aspects. AOSD Nicolas Tabareau
2010	J	`jnl`	How Synchronization Protects from Noise. PLoS Comput. Biol. Nicolas Tabareau, Jean-Jacques E. Slotine, Quang-Cuong Pham
2010	J	`jnl`	Resource modalities in tensor logic. Ann. Pure Appl. Log. Paul-André Melliès, Nicolas Tabareau
2009	J	`jnl`	A Contraction Theory Approach to Stochastic Incremental Stability. IEEE Trans. Autom. Control. Quang-Cuong Pham, Nicolas Tabareau, Jean-Jacques E. Slotine
2009	B	`conf`	An Algebraic Account of References in Game Semantics. MFPS Paul-André Melliès, Nicolas Tabareau
2009	—	`conf`	An Explicit Formula for the Free Exponential Modality of Linear Logic. ICALP (2) Paul-André Melliès, Nicolas Tabareau, Christine Tasson
2009	—	`conf`	Compiling functional types to relational specifications for low level imperative code. TLDI Nick Benton, Nicolas Tabareau
2008	—	`—`	Modalités de ressource et contrôle en logique tensorielle. (Resource modalities and control in tensorial logic). Nicolas Tabareau
2008	J	`jnl`	Where neuroscience and dynamic system theory meet autonomous robotics: A contracting basal ganglia model for action selection. Neural Networks Benoît Girard, Nicolas Tabareau, Quang-Cuong Pham, Alain Berthoz, Jean-Jacques E. Slotine
2007	J	`jnl`	Geometry of the superior colliculus mapping and efficient oculomotor computation. Biol. Cybern. Nicolas Tabareau, Daniel Bennequin, Alain Berthoz, Jean-Jacques E. Slotine, Benoît Girard
2007	J	`jnl`	Resource modalities in game semantics CoRR Paul-André Melliès, Nicolas Tabareau
2007	A*	`conf`	Resource modalities in game semantics. LICS Paul-André Melliès, Nicolas Tabareau
2006	J	`jnl`	De l'oprateur de trace dans les jeux de Conway CoRR Nicolas Tabareau
2006	—	`conf`	Implementation of a neurophysiological model of saccadic eye movements on an anthropomorphic robotic head. Humanoids Luigi Manfredi, Eliseo Stefano Maini, Paolo Dario, Cecilia Laschi, Benoît Girard, Nicolas Tabareau, Alain Berthoz
2006	J	`jnl`	On timed automata with input-determined guards CoRR Deepak D'Souza, Nicolas Tabareau
2004	—	`conf`	On Timed Automata with Input-Determined Guards. FORMATS/FTRTFT Deepak D'Souza, Nicolas Tabareau