Documentation
Français (FR)

Anglais (EN)

NT

Nicolas Tabareau

13

Documents

Présentation

Publications

911472

	The MetaCoq Project Matthieu Sozeau , Abhishek Anand , Simon Boulier , Cyril Cohen , Yannick Forster Journal of Automated Reasoning, 2020, ⟨10.1007/s10817-019-09540-0⟩ Article dans une revue hal-02167423v1
	Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq Matthieu Sozeau , Simon Boulier , Yannick Forster , Nicolas Tabareau , Théo Winterhalter Proceedings of the ACM on Programming Languages, 2020, pp.1-28. ⟨10.1145/3371076⟩ Article dans une revue hal-02380196v2
	Definitional Proof-Irrelevance without K Gaëtan Gilbert , Jesper Cockx , Matthieu Sozeau , Nicolas Tabareau Proceedings of the ACM on Programming Languages, 2019, POPL'19, pp.1-28. ⟨10.1145/329031610.1145/3290316⟩ Article dans une revue hal-01859964v2
	Equivalences for Free Nicolas Tabareau , Éric Tanter , Matthieu Sozeau Proceedings of the ACM on Programming Languages, 2018, ICFP'18, 2 (ICFP), pp.1-29. ⟨10.1145/3234615⟩ Article dans une revue hal-01559073v6

	From Lost to the River: Embracing Sort Proliferation Gaëtan Gilbert , Pierre-Marie Pédrot , Matthieu Sozeau , Nicolas Tabareau TYPES 2023 - 29th International Conference on Types for Proofs and Programs, Jun 2023, Valencia, Spain. pp.1-2 Communication dans un congrès hal-04378939v1
	Eliminating Reflection from Type Theory Théo Winterhalter , Matthieu Sozeau , Nicolas Tabareau CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Lisbonne, Portugal. pp.91-103, ⟨10.1145/3293880.3294095⟩ Communication dans un congrès hal-01849166v3
	Towards Certified Meta-Programming with Typed Template-Coq Abhishek Anand , Simon Boulier , Cyril Cohen , Matthieu Sozeau , Nicolas Tabareau ITP 2018 - 9th Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. pp.20-39, ⟨10.1007/978-3-319-94821-8_2⟩ Communication dans un congrès hal-01809681v1
	The Definitional Side of the Forcing Guilhem Jaber , Gabriel Lewertowski , Pierre-Marie Pédrot , Matthieu Sozeau , Nicolas Tabareau Logics in Computer Science, May 2016, New York, United States. ⟨10.1145/http://dx.doi.org/10.1145/2933575.2935320⟩ Communication dans un congrès hal-01319066v1
	Extending Type Theory with Forcing Guilhem Jaber , Nicolas Tabareau , Matthieu Sozeau LICS 2012 : Logic In Computer Science, Jun 2012, Dubrovnik, Croatia. pp.0-0 Communication dans un congrès hal-00685150v1

	Forcing in Coq Matthieu Sozeau , Nicolas Tabareau , Guilhem Jaber 2012 Autre publication scientifique hal-00767483v1

	Correct and Complete Type Checking and Certified Erasure for Coq, in Coq Matthieu Sozeau , Yannick Forster , Meven Lennon-Bertrand , Jakob Botsch Nielsen , Nicolas Tabareau 2023 Pré-publication, Document de travail hal-04077552v1
	Verified Extraction from Coq to OCaml Yannick Forster , Matthieu Sozeau , Nicolas Tabareau 2023 Pré-publication, Document de travail hal-04329663v1
	The Multiverse: Logical Modularity for Proof Assistants Kenji Maillard , Nicolas Margulies , Matthieu Sozeau , Nicolas Tabareau , Éric Tanter 2021 Pré-publication, Document de travail hal-03324596v1