Home » Fiche   membre
Fiche   membre Retour à l'annuaire  

Nicolas TABAREAU

CHERCHEUR

HDR

Equipe : GALLINETTE.

: Nicolas.Tabareauatls2n.fr

: 33

Adresse :

IMT Atlantique Bretagne-Pays de la Loire Ecole Mines-Telecom ( IMT ATLANTIQUE )
La Chantrerie
4, rue Alfred Kastler
B.P. 20722
44307 NANTES Cedex 3



Publications référencées sur HAL

Revues internationales avec comité de lecture (ART_INT)

    • [1] N. Tabareau, . Tanter, M. Sozeau. The Marriage of Univalence and Parametricity. In Journal of the ACM (JACM) ; éd. Association for Computing Machinery, 2021, vol. 68, num. 1.
      https://hal.inria.fr/hal-03120580
    • [3] M. Sozeau, S. Boulier, Y. Forster, N. Tabareau, T. Winterhalter. Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2020.
      https://hal.archives-ouvertes.fr/hal-02380196v2
    • [5] M. Sozeau, A. Anand, S. Boulier, C. Cohen, Y. Forster, F. Kunze, G. Malecha, N. Tabareau, T. Winterhalter. The MetaCoq Project. In Journal of Automated Reasoning ; éd. Springer Verlag, 2020.
      https://hal.inria.fr/hal-02167423
    • [6] S. Boulier, N. Tabareau. Model structure on the universe of all types in interval type theory. In Mathematical Structures in Computer Science ; éd. Cambridge University Press (CUP), 2020.
      https://hal.inria.fr/hal-02966633
    • [7] G. Gilbert, J. Cockx, M. Sozeau, N. Tabareau. Definitional Proof-Irrelevance without K. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2019.
      https://hal.inria.fr/hal-01859964v2
    • [8] N. Tabareau, . Tanter. Chemical foundations of distributed aspects. In Distributed Computing ; éd. Springer Verlag, 2019, vol. 32, num. 3.
      https://hal.inria.fr/hal-01811884
    • [9] P. Pédrot, N. Tabareau, H. Fehrmann, . Tanter. A Reasonably Exceptional Type Theory. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2019, vol. 3.
      https://hal.inria.fr/hal-02189128
    • [10] P. Dagand, N. Tabareau, . Tanter. Foundations of Dependent Interoperability. In Journal of Functional Programming ; éd. Cambridge University Press (CUP), 2018, vol. 28.
      https://hal.inria.fr/hal-01629909v2
    • [11] P. Melliès, N. Tabareau, C. Tasson. An explicit formula for the free exponential modality of linear logic. In Mathematical Structures in Computer Science ; éd. Cambridge University Press (CUP), 2018, vol. 28, num. 7.
      https://hal.inria.fr/hal-01992148
    • [12] N. Tabareau, . Tanter, M. Sozeau. Equivalences for Free. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2018, vol. 2, num. ICFP.
      https://hal.inria.fr/hal-01559073v6
    • [13] P. LeFanu Lumsdaine, N. Tabareau. Preface: Special Issue on Homotopy Type Theory and Univalent Foundations. In Journal of Automated Reasoning ; éd. Springer Verlag, 2018.
      https://hal.inria.fr/hal-01929871
    • [14] K. Quirin, N. Tabareau. Lawvere-Tierney sheafification in Homotopy Type Theory. In Journal of Formalized Reasoning ; éd. ASDD-AlmaDL, 2016, vol. 9, num. 2.
      https://hal.inria.fr/hal-01451710
    • [15] I. Figueroa, N. Tabareau, . Tanter. Effect capabilities for Haskell: Taming effect interference in monadic programming. In Science of Computer Programming ; éd. Elsevier, 2016, vol. 119.
      https://hal.inria.fr/hal-01400002
    • [16] I. Figueroa, N. Tabareau, . Tanter. Effective Aspects: A Typed Monadic Embedding of Pointcuts and Advice. In LNCS Transactions on Aspect-Oriented Software Development ; éd. Springer, 2014.
      https://hal.inria.fr/hal-00872782
    • [17] . Tanter, I. Figueroa, N. Tabareau. Execution Levels for Aspect-Oriented Programming: Design, Semantics, Implementations and Applications. In Science of Computer Programming ; éd. Elsevier, 2014, vol. 80, num. 1.
      https://hal.inria.fr/hal-00872786
    • [18] N. Tabareau, J. Slotine, Q. Pham. How synchronization protects from noise.. In PLoS Computational Biology ; éd. Public Library of Science, 2010, vol. 6, num. 1.
      https://hal.inria.fr/inria-00460739
    • [20] Q. Pham, N. Tabareau, J. Slotine. A contraction theory approach to stochastic incremental stability. In IEEE Transactions on Automatic Control ; éd. Institute of Electrical and Electronics Engineers, 2009, vol. 54, num. 4.
      https://hal.inria.fr/inria-00466264
    • [21] N. Tabareau, D. Bennequin, A. Berthoz, J. Slotine, B. Girard. Geometry of the superior colliculus mapping and efficient oculomotor computation. In Biological Cybernetics (Modeling) ; éd. Springer Verlag, 2007, vol. 97, num. 4.
      https://hal.archives-ouvertes.fr/hal-00178144

Conférences internationales avec comité de lecture et actes (COMM_INT)

    • [22] T. Winterhalter, M. Sozeau, N. Tabareau. Eliminating Reflection from Type Theory. In CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, janvier 2019, Lisbonne, Portugal.
      https://hal.archives-ouvertes.fr/hal-01849166v3
    • [23] T. Altenkirch, S. Boulier, A. Kaposi, N. Tabareau. Setoid type theory - a syntactic translation. In MPC 2019 - 13th International Conference on Mathematics of Program Construction, octobre 2019, Porto, Portugal.
      https://hal.inria.fr/hal-02281225
    • [24] A. Anand, S. Boulier, N. Tabareau, M. Sozeau. Typed Template Coq -- Certified Meta-Programming in Coq. In CoqPL 2018 - The Fourth International Workshop on Coq for Programming Languages, janvier 2018, Los Angeles, CA, états-Unis.
      https://hal.inria.fr/hal-01671948
    • [25] P. Pédrot, N. Tabareau. Failure is Not an Option An Exceptional Type Theory. In ESOP 2018 - 27th European Symposium on Programming, avril 2018, Thessaloniki, Grèce.
      https://hal.inria.fr/hal-01840643
    • [26] A. Anand, S. Boulier, C. Cohen, M. Sozeau, N. Tabareau. Towards Certified Meta-Programming with Typed Template-Coq. In ITP 2018 - 9th Conference on Interactive Theorem Proving, juillet 2018, Oxford, Royaume-Uni.
      https://hal.archives-ouvertes.fr/hal-01809681
    • [27] S. Boulier, P. Pédrot, N. Tabareau. The next 700 syntactical models of type theory. In Certified Programs and Proofs (CPP 2017), janvier 2017, Paris, France.
      https://hal.inria.fr/hal-01445835
    • [28] P. Pédrot, N. Tabareau. An Effectful Way to Eliminate Addiction to Dependence. In Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on, juin 2017, Reykjavik, Islande.
      https://hal.inria.fr/hal-01441829
    • [30] P. Dagand, N. Tabareau, . Tanter. Partial Type Equivalences for Verified Dependent Interoperability. In ICFP 2016 - 21st ACM SIGPLAN International Conference on Functional Programming, septembre 2016, Nara, Japon.
      https://hal.inria.fr/hal-01328012
    • [31] A. Hirschowitz, T. Hirschowitz, N. Tabareau. Wild omega-Categories for the Homotopy Hypothesis in Type Theory. In Typed Lambda Calculi and Applications, 2015, Varsovie, Pologne.
      https://hal.archives-ouvertes.fr/hal-01178301
    • [32] . Tanter, N. Tabareau. Gradual Certified Programming in Coq. In 11th ACM Dynamic Languages Symposium (DLS 2015), octobre 2015, Pittsburgh, états-Unis.
      https://hal.inria.fr/hal-01238774
    • [33] I. Figueroa, T. Schrijvers, N. Tabareau, . Tanter. Compositional Reasoning About Aspect Interference. In 13th International Conference on Modularity (Modularity'14), avril 2014, Lugano, Suisse.
      https://hal.inria.fr/hal-00919935
    • [34] N. Tabareau, M. Südholt, . Tanter. Aspectual Session Types. In Modularity - 13th International Conference on Modularity, avril 2014, Lugano, Suisse.
      https://hal.inria.fr/hal-00872791
    • [36] R. Douence, N. Tabareau. Lazier Imperative Programming. In Principles and Practice of Declarative Programming (PPDP), septembre 2014, Canterbury, Royaume-Uni.
      https://hal.inria.fr/hal-01016565
    • [37] I. Figueroa, N. Tabareau, . Tanter. Effect Capabilities For Haskell. In Brazilian Symposium on Programming Languages (SBLP), septembre 2014, Maceio, Brésil.
      https://hal.inria.fr/hal-01038053
    • [38] N. Tabareau, I. Figueroa, . Tanter. A Typed Monadic Embedding of Aspects. In 12th annual international conference on Aspect-Oriented Software Development (Modularity-AOSD'13), mars 2013, Fukuoka, Japon.
      https://hal.inria.fr/hal-00763695
    • [39] I. Figueroa, N. Tabareau, . Tanter. Taming aspects with monads and membranes. In FOAL'13: Foundations of aspect-oriented languages, mars 2013, Fukuoka, Japon.
      https://hal.inria.fr/hal-00808983
    • [40] I. Figueroa, . Tanter, N. Tabareau. A Practical Monadic Aspect Weaver. In Foundations of Aspect-Oriented Languages, mars 2012, Potsdam, Allemagne.
      https://hal.inria.fr/hal-00690717
    • [42] . Tanter, N. Tabareau, R. Douence. Taming Aspects with Membranes. In Foundations of Aspect-Oriented Languages, mars 2012, Potsdam, Allemagne.
      https://hal.inria.fr/hal-00690706
    • [44] N. Tabareau. Aspect oriented programming: a language for 2-categories. In Proceedings of the 10th international workshop on Foundations of aspect-oriented languages, mars 2011, Porto de Galinhas, Brésil.
      https://hal.inria.fr/inria-00583429
    • [45] N. Tabareau. A theory of distributed aspects. In 9th International Conference on Aspect-Oriented Software Development (AOSD '10), mars 2010, Rennes, Saint-Malo, France.In ACM (éds.), . , 2010.
      https://hal.inria.fr/inria-00423996v4
    • [46] N. Benton, N. Tabareau. Compiling Functional Types to Relational Specifications for Low Level Imperative Code. In Types in Language Design and Implementation, janvier 2009, Savannah, états-Unis.
      https://hal.archives-ouvertes.fr/hal-00341404
    • [47] P. Melliès, N. Tabareau, C. Tasson. An explicit formula for the free exponential modality of linear logic. In 36th International Colloquium on Automata, Languages and Programming, juillet 2009, Rhodes, Grèce.
      https://hal.archives-ouvertes.fr/hal-00391714v2
    • [48] P. Melliès, N. Tabareau. An algebraic account of references in game semantics. In Mathematical Foundations of Programming Semantics, avril 2009, Oxford, Royaume-Uni.In Electronic Notes in Theoretical Computer Science (éds.), Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics (MFPS 2009). , 2009.
      https://hal.archives-ouvertes.fr/hal-00374933v2
    • [49] P. Melliès, N. Tabareau, C. Tasson. An explicit formula for the free exponential modality of linear logic. In ICALP 2009 : 36th International Colloquium on Automata, Languages, and Programming, juillet 2009, Rhodes, Grèce.In Mathematical Structures in Computer Science ; éd. Cambridge University Press (CUP), 2009.
      https://hal.archives-ouvertes.fr/hal-02436316
    • [50] L. Manfredi, E. Maini, P. Dario, C. Laschi, B. Girard, N. Tabareau, A. Berthoz. Implementation of a neurophysiological model of saccadic eye movements on an anthropomorphic robotic head. In 6th IEEE-RAS International Conference on Humanoid Robots, décembre 2006, Gênes, Italie.
      https://hal.archives-ouvertes.fr/hal-01525198
    • [51] B. Girard, N. Tabareau, J. Slotine, A. Berthoz. Contracting model of the basal ganglia. In Modeling Natural Action Selection, 2005, Edinburgh, Royaume-Uni.In Bryson, J., Prescott, T. and Seth, A. (éds.), . AISB Press, 2005.
      https://hal.archives-ouvertes.fr/hal-00016414
    • [52] D. D'Souza, N. Tabareau. On timed automata with input-determined guards. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, septembre 2004, , France.In yassine Lakhnech (éds.), Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. springer-verlag, 2004.
      https://hal.archives-ouvertes.fr/hal-00017462

Conférences nationales avec comité de lecture et actes (COMM_NAT)

    • [53] S. Boulier, P. Pédrot, N. Tabareau. Modèles de la théorie des types donnés par traduction de programme. In 28ièmes Journées Francophones des Langages Applicatifs, janvier 2017, Gourette, France.
      https://hal.archives-ouvertes.fr/hal-01503089
    • [54] N. Tabareau, . Tanter, I. Figueroa. Anti-Unification with Type Classes. In Journées Francophones des Langages Applicatifs (JFLA), février 2013, Aussois, France.
      https://hal.inria.fr/hal-00765862
    • [55] G. Jaber, N. Tabareau. The Journey of Biorthogonal Logical Relations to the Realm of Assembly Code. In Workshop LOLA 2011, Syntax and Semantics of Low Level Languages, juin 2011, Toronto, Canada.
      https://hal.archives-ouvertes.fr/hal-00594386
    • [57] B. Girard, N. Tabareau, A. Berthoz, J. Slotine. Selective amplification using a contracting model of the basal ganglia. In NeuroComp 2006, 2006, Pont A Mousson, France.In Alexandre, F., Boniface, Y., Bougrain, L., Girau, B. and Rougier, N. (éds.), . , 2006.
      https://hal.archives-ouvertes.fr/hal-00111145

Theses et HDR (THESE)

Autres publications (AUTRES)

Copyright : LS2N 2017 - Mentions Légales - 
 -