Fiche membre Retour à l'annuaire
![](http://www.ls2n.fr/wp-content/plugins/annuaireLS2N/img/neutral_avatar.png)
Nicolas TABAREAU
CHERCHEUR
HDR
: Nicolas.Tabareauatls2n.fr
Adresse :
IMT Atlantique Bretagne-Pays de la Loire Ecole Mines-Telecom ( IMT ATLANTIQUE )La Chantrerie4, rue Alfred KastlerB.P. 20722
44307 NANTES Cedex 3
Publications référencées sur HAL
![](https://hal.archives-ouvertes.fr/img/tamponHal.png)
Revues internationales avec comité de lecture (ART_INT)
- [1] Y. Forster, M. Sozeau, N. Tabareau. Verified Extraction from Coq to OCaml. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2024, vol. 8, num. PLDI.https://inria.hal.science/hal-04329663
- [2] M. Malewski, K. Maillard, N. Tabareau, Ã. Tanter. Gradual Indexed Inductive Types. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2024, vol. 8, num. ICFP.https://inria.hal.science/hal-04681546
- [3] L. Pujet, N. Tabareau. Impredicative Observational Equality. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2023, vol. 7, num. POPL.https://hal.science/hal-03857705v2
- [4] M. Lennon-Bertrand, K. Maillard, N. Tabareau, Ã. Tanter. Gradualizing the Calculus of Inductive Constructions. In ACM Transactions on Programming Languages and Systems (TOPLAS) ; éd. ACM, 2022.https://hal.science/hal-02896776v5
- [5] K. Maillard, M. Lennon-Bertrand, N. Tabareau, Ã. Tanter. A Reasonably Gradual Type Theory. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2022.https://inria.hal.science/hal-03596652v2
- [6] L. Pujet, N. Tabareau. Observational Equality: Now For Good. In POPL 2022: Symposium on Principles of Programming Languages, janvier 2022, Philadelphia, états-Unis.In Proceedings of the ACM on Programming Languages ; éd. ACM, 2022, vol. 6, num. POPL.https://inria.hal.science/hal-03367052v4
- [7] J. Cockx, N. Tabareau, T. Winterhalter. The Taming of the Rew: A Type Theory with Computational Assumptions. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2021.https://hal.science/hal-02901011v2
- [8] 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://inria.hal.science/hal-03120580
- [9] 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.science/hal-02380196v2
- [10] P. Pédrot, N. Tabareau. The Fire Triangle. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2020.https://hal.science/hal-02383109
- [11] 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://inria.hal.science/hal-02167423
- [12] 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://inria.hal.science/hal-02966633
- [13] 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://inria.hal.science/hal-01859964v2
- [14] N. Tabareau, Ã. Tanter. Chemical foundations of distributed aspects. In Distributed Computing ; éd. Springer Verlag, 2019, vol. 32, num. 3.https://inria.hal.science/hal-01811884
- [15] 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://inria.hal.science/hal-02189128
- [16] P. Dagand, N. Tabareau, Ã. Tanter. Foundations of Dependent Interoperability. In Journal of Functional Programming ; éd. Cambridge University Press (CUP), 2018, vol. 28.https://inria.hal.science/hal-01629909v2
- [17] 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://inria.hal.science/hal-01992148
- [18] N. Tabareau, Ã. Tanter, M. Sozeau. Equivalences for Free. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2018, vol. 2, num. ICFP.https://inria.hal.science/hal-01559073v6
- [19] 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://inria.hal.science/hal-01929871
- [20] 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://inria.hal.science/hal-01451710
- [21] 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://inria.hal.science/hal-01400002
- [22] 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://inria.hal.science/hal-00872782
- [23] Ã. 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://inria.hal.science/hal-00872786
- [24] N. Tabareau, J. Slotine, Q. Pham. How synchronization protects from noise.. In PLoS Computational Biology ; éd. PLOS, 2010, vol. 6, num. 1.https://inria.hal.science/inria-00460739
- [25] P. Melliès, N. Tabareau. Resource modalities in tensor logic. In Annals of Pure and Applied Logic ; éd. Elsevier Masson, 2010, vol. 161, num. 5.https://hal.science/hal-00339154v2
- [26] 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://inria.hal.science/inria-00466264
- [27] 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.science/hal-00178144
- [28] L. Pujet, N. Tabareau. Observational Equality Meets CIC. In ESOP 2024 - 33rd European Symposium on Programming, avril 2024, Luxembourg, Luxembourg.https://hal.science/hal-04535982
- [29] G. Gilbert, P. Pédrot, M. Sozeau, N. Tabareau. From Lost to the River: Embracing Sort Proliferation. In TYPES 2023 - 29th International Conference on Types for Proofs and Programs, juin 2023, Valencia, Espagne.https://inria.hal.science/hal-04378939
- [30] G. Gilbert, Y. Leray, N. Tabareau, T. Winterhalter. The Rewster: The Coq Proof Assistant with Rewrite Rules. In TYPES 2023 - 29th International Conference on Types for Proofs and Programs, juin 2023, Valencia, Espagne.https://inria.hal.science/hal-04403667
- [31] 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.science/hal-01849166v3
- [32] 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://inria.hal.science/hal-02281225
- [33] 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://inria.hal.science/hal-01671948
- [34] 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://inria.hal.science/hal-01840643
- [35] 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.science/hal-01809681
- [36] 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://inria.hal.science/hal-01445835
- [37] 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://inria.hal.science/hal-01441829
- [38] G. Jaber, G. Lewertowski, P. Pédrot, M. Sozeau, N. Tabareau. The Definitional Side of the Forcing. In Logics in Computer Science, mai 2016, New York, états-Unis.https://hal.science/hal-01319066
- [39] 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://inria.hal.science/hal-01328012
- [40] 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.science/hal-01178301
- [41] Ã. Tanter, N. Tabareau. Gradual Certified Programming in Coq. In 11th ACM Dynamic Languages Symposium (DLS 2015), octobre 2015, Pittsburgh, états-Unis.https://inria.hal.science/hal-01238774
- [42] 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://inria.hal.science/hal-00919935
- [43] N. Tabareau, M. Südholt, Ã. Tanter. Aspectual Session Types. In Modularity - 13th International Conference on Modularity, avril 2014, Lugano, Suisse.https://inria.hal.science/hal-00872791
- [44] M. Sozeau, N. Tabareau. Universe Polymorphism in Coq. In Interactive Theorem Proving, juillet 2014, Vienna, Autriche.https://inria.hal.science/hal-00974721
- [45] R. Douence, N. Tabareau. Lazier Imperative Programming. In Principles and Practice of Declarative Programming (PPDP), septembre 2014, Canterbury, Royaume-Uni.https://inria.hal.science/hal-01016565
- [46] I. Figueroa, N. Tabareau, Ã. Tanter. Effect Capabilities For Haskell. In Brazilian Symposium on Programming Languages (SBLP), septembre 2014, Maceio, Brésil.https://inria.hal.science/hal-01038053
- [47] 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://inria.hal.science/hal-00763695
- [48] I. Figueroa, N. Tabareau, Ã. Tanter. Taming aspects with monads and membranes. In FOAL'13: Foundations of aspect-oriented languages, mars 2013, Fukuoka, Japon.https://inria.hal.science/hal-00808983
- [49] I. Figueroa, Ã. Tanter, N. Tabareau. A Practical Monadic Aspect Weaver. In Foundations of Aspect-Oriented Languages, mars 2012, Potsdam, Allemagne.https://inria.hal.science/hal-00690717
- [50] N. Tabareau. A Monadic Interpretation of Execution Levels and Exceptions for AOP. In Modularity: AOSD'12, mars 2012, Postdam, Allemagne.https://inria.hal.science/inria-00592132v3
- [51] Ã. Tanter, N. Tabareau, R. Douence. Taming Aspects with Membranes. In Foundations of Aspect-Oriented Languages, mars 2012, Potsdam, Allemagne.https://inria.hal.science/hal-00690706
- [52] G. Jaber, N. Tabareau, M. Sozeau. Extending Type Theory with Forcing. In LICS 2012 : Logic In Computer Science, juin 2012, Dubrovnik, Croatie.https://hal.science/hal-00685150
- [53] 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://inria.hal.science/inria-00583429
- [54] 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://inria.hal.science/inria-00423996v4
- [55] 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.science/hal-00341404
- [56] 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.science/hal-00391714v2
- [57] 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.science/hal-00374933v2
- [58] 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.science/hal-02436316
- [59] 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.science/hal-01525198
- [60] 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.science/hal-00016414
- [61] 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.science/hal-00017462
- [62] 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.science/hal-01503089
- [63] N. Tabareau, Ã. Tanter, I. Figueroa. Anti-Unification with Type Classes. In Journées Francophones des Langages Applicatifs (JFLA), février 2013, Aussois, France.https://inria.hal.science/hal-00765862
- [64] 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.science/hal-00594386
- [65] G. Jaber, N. Tabareau. Krivine realizability for compiler correctness. In Workshop LOLA 2010, Syntax and Semantics of Low Level Languages, juillet 2010, Edinburgh, Royaume-Uni.https://hal.science/hal-00475210v2
- [66] 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.science/hal-00111145
- [67] N. Tabareau. Managing Logical and Computational Complexity using Program Transformations. https://theses.hal.science/tel-01406351
- [68] N. Tabareau. Modalités de ressource et contrôle en logique tensorielle. Thèses : Université Paris-Diderot - Paris VII. https://theses.hal.science/tel-00339149v3
- [69] R. Douence, N. Tabareau. Lazier Imperative Programming. Rapport technique, 2014 ; INRIA.https://inria.hal.science/hal-01025633v2
- [70] N. Tabareau, J. Slotine. Contraction analysis of nonlinear random dynamical systems. Rapport technique, 2013 ; INRIA.https://inria.hal.science/hal-00864079v2
- [71] M. Sozeau, N. Tabareau, G. Jaber. Forcing in Coq. https://inria.hal.science/hal-00767483
- [72] N. Tabareau. Aspect Oriented Programming: a language for 2-categories. Rapport technique, 2011 ; INRIA.https://inria.hal.science/inria-00470400v3
- [73] Ã. Tanter, N. Tabareau, R. Douence. Exploring Membranes for Controlling Aspects. Rapport technique, 2011 ; INRIA.https://inria.hal.science/inria-00592133v2