Number of documents

68

Page de publications de Nicolas Tabareau


Journal articles14 documents

  • Nicolas Tabareau, Éric Tanter. Chemical foundations of distributed aspects. Distributed Computing, Springer Verlag, In press, 32 (Issue 3), pp.193-216. ⟨10.1007/s00446-018-0334-6⟩. ⟨hal-01811884⟩
  • Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau. Definitional Proof-Irrelevance without K. Proceedings of the ACM on Programming Languages, ACM, 2019, POPL'19, pp.1-28. ⟨10.1145/329031610.1145/3290316⟩. ⟨hal-01859964v2⟩
  • Peter Lefanu Lumsdaine, Nicolas Tabareau. Preface: Special Issue on Homotopy Type Theory and Univalent Foundations. Journal of Automated Reasoning, Springer Verlag, 2018, ⟨10.1007/s10817-018-9491-3⟩. ⟨hal-01929871⟩
  • Nicolas Tabareau, Éric Tanter, Matthieu Sozeau. Equivalences for Free: Univalent Parametricity for Effective Transport. Proceedings of the ACM on Programming Languages, ACM, 2018, ICFP'18, 2 (ICFP), pp.1-29. ⟨10.1145/3234615⟩. ⟨hal-01559073v6⟩
  • Paul-André Melliès, Nicolas Tabareau, Christine Tasson. An explicit formula for the free exponential modality of linear logic. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, 28 (7), pp.1253-1286. ⟨10.1017/S0960129516000426⟩. ⟨hal-01992148⟩
  • Pierre-Evariste Dagand, Nicolas Tabareau, Éric Tanter. Foundations of Dependent Interoperability. Journal of Functional Programming, Cambridge University Press (CUP), 2018, 28, ⟨10.1017/S0956796818000011⟩. ⟨hal-01629909v2⟩
  • Kevin Quirin, Nicolas Tabareau. Lawvere-Tierney sheafification in Homotopy Type Theory. Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (2), ⟨10.6092/issn.1972-5787/6232⟩. ⟨hal-01451710⟩
  • Ismael Figueroa, Nicolas Tabareau, Éric Tanter. Effect capabilities for Haskell: Taming effect interference in monadic programming. Science of Computer Programming, Elsevier, 2016, 119, pp.3-30. ⟨10.1016/j.scico.2015.11.010⟩. ⟨hal-01400002⟩
  • Ismael Figueroa, Nicolas Tabareau, Éric Tanter. Effective Aspects: A Typed Monadic Embedding of Pointcuts and Advice. Transactions on Aspect-Oriented Software Development, LNCS, 2014. ⟨hal-00872782⟩
  • Éric Tanter, Ismael Figueroa, Nicolas Tabareau. Execution Levels for Aspect-Oriented Programming: Design, Semantics, Implementations and Applications. Science of Computer Programming, Elsevier, 2014, 80 (1), pp.311-342. ⟨10.1016/j.scico.2013.09.002⟩. ⟨hal-00872786⟩
  • Nicolas Tabareau, Jean-Jacques Slotine, Quang-Cuong Pham. How synchronization protects from noise.. PLoS Computational Biology, Public Library of Science, 2010, 6 (1), pp.e1000637. ⟨10.1371/journal.pcbi.1000637⟩. ⟨inria-00460739⟩
  • Paul-André Melliès, Nicolas Tabareau. Resource modalities in tensor logic. Annals of Pure and Applied Logic, Elsevier Masson, 2010, 161 (5), pp.632-653. ⟨10.1016/j.apal.2009.07.018⟩. ⟨hal-00339154v2⟩
  • Quang-Cuong Pham, Nicolas Tabareau, Jean-Jacques Slotine. A contraction theory approach to stochastic incremental stability. IEEE Transactions on Automatic Control, Institute of Electrical and Electronics Engineers, 2009, 54 (4), pp.816--820. ⟨10.1109/TAC.2008.2009619⟩. ⟨inria-00466264⟩
  • Nicolas Tabareau, Daniel Bennequin, Alain Berthoz, Jean-Jacques Slotine, Benoît Girard. Geometry of the superior colliculus mapping and efficient oculomotor computation. Biological Cybernetics (Modeling), Springer Verlag, 2007, 97 (4), pp.279-292. ⟨10.1007/s00422-007-0172-2⟩. ⟨hal-00178144⟩

Conference papers36 documents

  • Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau. Eliminating Reflection from Type Theory: To the Legacy of Martin Hofmann. CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Lisbonne, Portugal. pp.91-103, ⟨10.1145/3293880.3294095⟩. ⟨hal-01849166v3⟩
  • Pierre-Marie Pédrot, Nicolas Tabareau, Hans Fehrmann, Éric Tanter. A Reasonably Exceptional Type Theory. ICFP 2019 - 24th ACM SIGPLAN International Conference on Functional Programming, Aug 2019, Berlin, Germany. pp.1-29, ⟨10.1145/3341712⟩. ⟨hal-02189128⟩
  • Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau. Setoid type theory - a syntactic translation. MPC 2019 - 13th International Conference on Mathematics of Program Construction, Oct 2019, Porto, Portugal. pp.155-196, ⟨10.1007/978-3-030-33636-3_7⟩. ⟨hal-02281225⟩
  • 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/http://dx.doi.org/10.1145/2933575.2935320⟩. ⟨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⟩
  • 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⟩
  • Matthieu Sozeau, Nicolas Tabareau. Universe Polymorphism in Coq. Interactive Theorem Proving, Jul 2014, Vienna, Austria. ⟨hal-00974721⟩
  • Ismael Figueroa, Nicolas Tabareau, Éric Tanter. Effect Capabilities For Haskell. Brazilian Symposium on Programming Languages (SBLP), Sep 2014, Maceio, Brazil. ⟨hal-01038053⟩
  • 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⟩
  • 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⟩
  • 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〉
  • Nicolas Tabareau. A Monadic Interpretation of Execution Levels and Exceptions for AOP. Modularity: AOSD'12, Mar 2012, Postdam, Germany. ⟨inria-00592132v3⟩
  • Ismael Figueroa, Éric Tanter, Nicolas Tabareau. A Practical Monadic Aspect Weaver. Foundations of Aspect-Oriented Languages, Mar 2012, Potsdam, Germany. ⟨hal-00690717⟩
  • Éric Tanter, Nicolas Tabareau, Rémi Douence. Taming Aspects with Membranes. Foundations of Aspect-Oriented Languages, Mar 2012, Potsdam, Germany. ⟨hal-00690706⟩
  • 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⟩
  • 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⟩
  • 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⟩
  • 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⟩
  • 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, ...11 documents

  • Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, et al.. The MetaCoq Project. 2019. ⟨hal-02167423⟩
  • 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. De l'opérateur de trace dans les jeux de Conway. 2006. ⟨hal-00086635⟩
  • Nicolas Tabareau, Jean-Jacques Slotine. Notes on Contraction Theory. 2006. ⟨hal-00016453v2⟩

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⟩
  • Éric Tanter, Nicolas Tabareau, Rémi Douence. Exploring Membranes for Controlling Aspects. [Research Report] RR-7739, INRIA. 2011, pp.33. ⟨inria-00592133v2⟩
  • Nicolas Tabareau. Aspect Oriented Programming: a language for 2-categories. [Research Report] RR-7527, INRIA. 2011, pp.30. ⟨inria-00470400v3⟩

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⟩