Number of documents


Page de publications de Nicolas Tabareau

Journal articles14 documents

Conference papers34 documents

  • Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau. Eliminating Reflection from Type Theory: To the Legacy of Martin Hofmann. CPP 2019 - The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Lisbonne, Portugal. pp.91-103, ⟨10.1145/3293880.3294095⟩. ⟨hal-01849166v3⟩
  • Abhishek Anand, Simon Boulier, Nicolas Tabareau, Matthieu Sozeau. Typed Template Coq -- Certified Meta-Programming in Coq. CoqPL 2018 - The Fourth International Workshop on Coq for Programming Languages, Jan 2018, Los Angeles, CA, United States. pp.1-2. ⟨hal-01671948⟩
  • Pierre-Marie Pédrot, Nicolas Tabareau. Failure is Not an Option An Exceptional Type Theory. ESOP 2018 - 27th European Symposium on Programming, Apr 2018, Thessaloniki, Greece. pp.245-271, ⟨10.1007/978-3-319-89884-1_9⟩. ⟨hal-01840643⟩
  • Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau. Towards Certified Meta-Programming with Typed Template-Coq. ITP 2018 - 9th Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. pp.20-39, ⟨10.1007/978-3-319-94821-8_2⟩. ⟨hal-01809681⟩
  • Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau. The next 700 syntactical models of type theory. Certified Programs and Proofs (CPP 2017), Jan 2017, Paris, France. pp.182 - 194, ⟨10.1145/3018610.3018620⟩. ⟨hal-01445835⟩
  • Pierre-Marie Pédrot, Nicolas Tabareau. An Effectful Way to Eliminate Addiction to Dependence. Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on, Jun 2017, Reykjavik, Iceland. pp.12, ⟨10.1109/LICS.2017.8005113⟩. ⟨hal-01441829⟩
  • Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau. Modèles de la théorie des types donnés par traduction de programme. 28ièmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France. ⟨hal-01503089⟩
  • Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau. The Definitional Side of the Forcing. Logics in Computer Science, May 2016, New York, United States. ⟨10.1145/⟩. ⟨hal-01319066⟩
  • Pierre-Evariste Dagand, Nicolas Tabareau, Éric Tanter. Partial Type Equivalences for Verified Dependent Interoperability. ICFP 2016 - 21st ACM SIGPLAN International Conference on Functional Programming, Sep 2016, Nara, Japan. pp.298-310, ⟨10.1145/2951913.2951933⟩. ⟨hal-01328012⟩
  • André Hirschowitz, Tom Hirschowitz, Nicolas Tabareau. Wild omega-Categories for the Homotopy Hypothesis in Type Theory. Typed Lambda Calculi and Applications, 2015, Varsovie, Poland. pp.226-240, ⟨10.4230/LIPIcs.TLCA.2015.226⟩. ⟨hal-01178301⟩
  • Éric Tanter, Nicolas Tabareau. Gradual Certified Programming in Coq. 11th ACM Dynamic Languages Symposium (DLS 2015), Oct 2015, Pittsburgh, United States. ⟨10.1145/2816707.2816710⟩. ⟨hal-01238774⟩
  • Rémi Douence, Nicolas Tabareau. Lazier Imperative Programming. Principles and Practice of Declarative Programming (PPDP), Sep 2014, Canterbury, United Kingdom. ⟨hal-01016565⟩
  • Ismael Figueroa, Nicolas Tabareau, Éric Tanter. Effect Capabilities For Haskell. Brazilian Symposium on Programming Languages (SBLP), Sep 2014, Maceio, Brazil. ⟨hal-01038053⟩
  • Nicolas Tabareau, Mario Südholt, Éric Tanter. Aspectual Session Types. Modularity - 13th International Conference on Modularity, Apr 2014, Lugano, Switzerland. ⟨10.1145/2577080.2577085⟩. ⟨hal-00872791⟩
  • Ismael Figueroa, Tom Schrijvers, Nicolas Tabareau, Éric Tanter. Compositional Reasoning About Aspect Interference. 13th International Conference on Modularity (Modularity'14), Apr 2014, Lugano, Switzerland. ⟨hal-00919935⟩
  • Matthieu Sozeau, Nicolas Tabareau. Universe Polymorphism in Coq. Interactive Theorem Proving, Jul 2014, Vienna, Austria. ⟨hal-00974721⟩
  • Nicolas Tabareau, Éric Tanter, Ismael Figueroa. Anti-Unification with Type Classes. Journées Francophones des Langages Applicatifs (JFLA), Feb 2013, Aussois, France. ⟨hal-00765862⟩
  • Nicolas Tabareau, Ismael Figueroa, Éric Tanter. A Typed Monadic Embedding of Aspects. 12th annual international conference on Aspect-Oriented Software Development (Modularity-AOSD'13), Mar 2013, Fukuoka, Japan. ⟨hal-00763695⟩
  • Ismael Figueroa, Nicolas Tabareau, Éric Tanter. Taming aspects with monads and membranes. FOAL'13: Foundations of aspect-oriented languages, Mar 2013, Fukuoka, Japan. ⟨10.1145/2451598.2451600⟩. ⟨hal-00808983⟩
  • Nicolas Tabareau. A Monadic Interpretation of Execution Levels and Exceptions for AOP. Modularity: AOSD'12, Mar 2012, Postdam, Germany. ACM Press, 2012. 〈inria-00592132v3〉
  • Éric Tanter, Nicolas Tabareau, Rémi Douence. Taming Aspects with Membranes. Foundations of Aspect-Oriented Languages, Mar 2012, Potsdam, Germany. 2012. 〈hal-00690706〉
  • Ismael Figueroa, Éric Tanter, Nicolas Tabareau. A Practical Monadic Aspect Weaver. Foundations of Aspect-Oriented Languages, Mar 2012, Potsdam, Germany. 2012. 〈hal-00690717〉
  • Guilhem Jaber, Nicolas Tabareau, Matthieu Sozeau. Extending Type Theory with Forcing. LICS 2012 : Logic In Computer Science, Jun 2012, Dubrovnik, Croatia. pp.0-0, 2012. 〈hal-00685150〉
  • Guilhem Jaber, Nicolas Tabareau. The Journey of Biorthogonal Logical Relations to the Realm of Assembly Code. Workshop LOLA 2011, Syntax and Semantics of Low Level Languages, Jun 2011, Toronto, Canada. ⟨hal-00594386⟩
  • Nicolas Tabareau. Aspect oriented programming: a language for 2-categories. Proceedings of the 10th international workshop on Foundations of aspect-oriented languages, Mar 2011, Porto de Galinhas, Brazil. pp.13--17, ⟨10.1145/1960510.1960514⟩. ⟨inria-00583429⟩
  • Nicolas Tabareau. A theory of distributed aspects. 9th International Conference on Aspect-Oriented Software Development (AOSD '10), Mar 2010, Rennes, Saint-Malo, France. pp.133--144, ⟨10.1145/1739230.1739246⟩. ⟨inria-00423996v4⟩
  • Guilhem Jaber, Nicolas Tabareau. Krivine realizability for compiler correctness. Workshop LOLA 2010, Syntax and Semantics of Low Level Languages, Jul 2010, Edinburgh, United Kingdom. ⟨hal-00475210v2⟩
  • Paul-André Melliès, Nicolas Tabareau, Christine Tasson. An explicit formula for the free exponential modality of linear logic. 36th International Colloquium on Automata, Languages and Programming, Jul 2009, Rhodes, Greece. pp.247-260, ⟨10.1007/978-3-642-02930-1⟩. ⟨hal-00391714v2⟩
  • Paul-André Melliès, Nicolas Tabareau. An algebraic account of references in game semantics. Mathematical Foundations of Programming Semantics, Apr 2009, Oxford, United Kingdom. pp.377-405, ⟨10.1016⟩. ⟨hal-00374933v2⟩
  • Nick Benton, Nicolas Tabareau. Compiling Functional Types to Relational Specifications for Low Level Imperative Code. Types in Language Design and Implementation, Jan 2009, Savannah, United States. ⟨hal-00341404⟩
  • Benoît Girard, Nicolas Tabareau, Alain Berthoz, Jean-Jacques Slotine. Selective amplification using a contracting model of the basal ganglia. NeuroComp 2006, 2006, Pont A Mousson, France. pp.30-33. ⟨hal-00111145⟩
  • Luigi Manfredi, Eliseo Stefano Maini, Paolo Dario, Cecilia Laschi, Benoît Girard, et al.. Implementation of a neurophysiological model of saccadic eye movements on an anthropomorphic robotic head. 6th IEEE-RAS International Conference on Humanoid Robots, Dec 2006, Gênes, Italy. pp.438-443, ⟨10.1109/ICHR.2006.321309⟩. ⟨hal-01525198⟩
  • Benoît Girard, Nicolas Tabareau, Jean-Jacques Slotine, Alain Berthoz. Contracting model of the basal ganglia. Modeling Natural Action Selection, 2005, Edinburgh, United Kingdom. pp.69-76. ⟨hal-00016414⟩
  • Deepak d'Souza, Nicolas Tabareau. On timed automata with input-determined guards. Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Sep 2004, France. pp.68-83, ⟨10.1007/b100824⟩. ⟨hal-00017462⟩

Other publications1 document

  • Matthieu Sozeau, Nicolas Tabareau, Guilhem Jaber. Forcing in Coq. 2012. ⟨hal-00767483⟩

Preprints, Working Papers, ...10 documents

  • Simon Boulier, Nicolas Tabareau. Model structure on the universe in a two level type theory. 2017. ⟨hal-01579822⟩
  • Matthieu Sozeau, Nicolas Tabareau. Univalence for free. 2013. ⟨hal-00786589v3⟩
  • Guilhem Jaber, Nicolas Tabareau. Decomposing Logical Relations with Forcing. 2011. ⟨hal-00585717⟩
  • Hervé Grall, Nicolas Tabareau. Linear logic as a foundation for service-oriented computing. 2010. ⟨inria-00473854v2⟩
  • Paul-André Melliès, Nicolas Tabareau. Free models of T-algebraic theories computed as Kan extensions. 2008. ⟨hal-00339331⟩
  • Paul-André Melliès, Nicolas Tabareau. Resource modalities in game semantics. 2007. ⟨hal-00144510⟩
  • Paul-André Melliès, Nicolas Tabareau. Linear continuations and duality. 2007. ⟨hal-00339156⟩
  • Nicolas Tabareau, Benoît Girard, Daniel Bennequin, Alain Berthoz, Jean-Jacques Slotine. Superior Colliculus geometry for spatio-temporal transformation. 2006. ⟨hal-00016885⟩
  • Nicolas Tabareau, Jean-Jacques Slotine. Notes on Contraction Theory. 2006. ⟨hal-00016453v2⟩
  • Nicolas Tabareau. De l'opérateur de trace dans les jeux de Conway. 2006. ⟨hal-00086635⟩

Reports4 documents

  • Rémi Douence, Nicolas Tabareau. Lazier Imperative Programming. [Research Report] RR-8569, INRIA. 2014. ⟨hal-01025633v2⟩
  • Nicolas Tabareau, Jean-Jacques Slotine. Contraction analysis of nonlinear random dynamical systems. [Research Report] RR-8368, INRIA. 2013, pp.17. ⟨hal-00864079v2⟩
  • Nicolas Tabareau. Aspect Oriented Programming: a language for 2-categories. [Research Report] RR-7527, INRIA. 2011, pp.30. ⟨inria-00470400v3⟩
  • Éric Tanter, Nicolas Tabareau, Rémi Douence. Exploring Membranes for Controlling Aspects. [Research Report] RR-7739, INRIA. 2011, pp.33. ⟨inria-00592133v2⟩

Theses1 document

  • Nicolas Tabareau. Modalités de ressource et contrôle en logique tensorielle. Mathématiques [math]. Université Paris-Diderot - Paris VII, 2008. Français. ⟨tel-00339149v3⟩

Habilitation à diriger des recherches1 document

  • Nicolas Tabareau. Managing Logical and Computational Complexity using Program Transformations. Category Theory [math.CT]. université de nantes, 2016. ⟨tel-01406351⟩