2024
Journal articles
- titre
- Gradual Indexed Inductive Types
- auteur
- Mara Malewski, Kenji Maillard, Nicolas Tabareau, Éric Tanter
- article
- Proceedings of the ACM on Programming Languages, 2024, 8 (ICFP), pp.544-572. ⟨10.1145/3674644⟩
- typdoc
- Journal articles
- Accès au bibtex
-
- titre
- Verified Extraction from Coq to OCaml
- auteur
- Yannick Forster, Matthieu Sozeau, Nicolas Tabareau
- article
- Proceedings of the ACM on Programming Languages, 2024, 8 (PLDI), pp.52-75. ⟨10.1145/3656379⟩
- typdoc
- Journal articles
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
- auteur
- Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter
- article
- International Conference on Interactive Theorem Proving (ITP 2024), Yves Bertot; Temur Kutsia; Michael Norrish, Sep 2024, Tbilisi, Georgia. pp.18, ⟨10.4230/LIPIcs.ITP.2024.26⟩
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- $\partial$ is for Dialectica
- auteur
- Marie Kerjean, Pierre-Marie Pédrot
- article
- LICS 2024 - 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2024, Tallinn, Estonia. pp.1-13
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Upon This Quote I Will Build My Church Thesis
- auteur
- Pierre-Marie Pédrot
- article
- LICS 2024 - 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2024, Tallin, Estonia. pp.1-12, ⟨10.1145/3661814.3662070⟩
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Observational Equality Meets CIC
- auteur
- Loïc Pujet, Nicolas Tabareau
- article
- ESOP 2024 - 33rd European Symposium on Programming, Apr 2024, Luxembourg, Luxembourg. pp.275-301, ⟨10.1007/978-3-031-57262-3_12⟩
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence
- auteur
- Cyril Cohen, Enzo Crance, Assia Mahboubi
- article
- ESOP 2024 - 33rd European Symposium on Programming, Apr 2024, Luxembourg, Luxembourg. pp.269-274, ⟨10.1007/978-3-031-57262-3_11⟩
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Trocq: Proof Transfer for Free, With or Without Univalence
- auteur
- Cyril Cohen, Enzo Crance, Assia Mahboubi
- article
- ESOP 2024 - 33rd European Symposium on Programming, Apr 2024, Luxembourg, Luxembourg. pp.239-268
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Composing Biases by Using CP to Decompose Minimal Functional Dependencies for Acquiring Complex Formulae
- auteur
- Ramiz Gindullin, Nicolas Beldiceanu, Jovial Cheukam-Ngouonou, Rémi Douence, Claude-Guy Quimper
- article
- AAAI 2024 - 38th Annual AAAI Conference on Artificial Intelligence, Feb 2024, Vancouver, Canada
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- A First Order Theory of Diagram Chasing
- auteur
- Assia Mahboubi, Matthieu Piquerez
- article
- CSL 2024 - 32nd EACSL Annual Conference on Computer Science Logic, Feb 2024, Naples, Italy. pp.1-19
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Modular efficient deconstruction with typed pointer reversal
- auteur
- Jean Caspar, Guillaume Munch-Maccagnoni
- article
- 35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- Martin-Löf à la Coq
- auteur
- Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet
- article
- 2024
- typdoc
- Preprints, Working Papers, ...
- Accès au texte intégral et bibtex
-
- titre
- Machine-Checked Categorical Diagrammatic Reasoning
- auteur
- Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez
- article
- 2024
- typdoc
- Preprints, Working Papers, ...
- Accès au texte intégral et bibtex
-
2023
Journal articles
- titre
- SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
- auteur
- Philipp Haselwarter, Exequiel Rivas, Antoine van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Cătălin Hriţcu, Kenji Maillard, Bas Spitters
- article
- ACM Transactions on Programming Languages and Systems (TOPLAS), 2023, 45 (3), pp.1-61. ⟨10.1145/3594735⟩
- typdoc
- Journal articles
- Accès au texte intégral et bibtex
-
- titre
- Impredicative Observational Equality
- auteur
- Loïc Pujet, Nicolas Tabareau
- article
- Proceedings of the ACM on Programming Languages, 2023, Proceedings of the ACM on programming languages, 7 (POPL), pp.74. ⟨10.1145/3571739⟩
- typdoc
- Journal articles
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Resource polymorphism: proposal for integrating first-class resources into ML
- auteur
- Guillaume Munch-Maccagnoni
- article
- Higher-order, Typed, Inferred, Strict: ML Family Workshop 2023, Oleg Kyseliov, Sep 2023, Seattle, United States
- typdoc
- Conference papers
- Accès au bibtex
-
- titre
- From Lost to the River: Embracing Sort Proliferation
- auteur
- Gaëtan Gilbert, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau
- article
- TYPES 2023 - 29th International Conference on Types for Proofs and Programs, Jun 2023, Valencia, Spain. pp.1-2
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- The Rewster: The Coq Proof Assistant with Rewrite Rules
- auteur
- Gaëtan Gilbert, Yann Leray, Nicolas Tabareau, Théo Winterhalter
- article
- TYPES 2023 - 29th International Conference on Types for Proofs and Programs, Jun 2023, Valencia, Spain. pp.1-3
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Manifest Termination
- auteur
- Assia Mahboubi, Guillaume Melquiond
- article
- TYPES 2023 - 29th International Conference on Types for Proofs and Programs, Jun 2023, Valencia, Spain. pp.1-3
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Boolean-Arithmetic Equations: Acquisition and Uses
- auteur
- R Gindullin, Nicolas Beldiceanu, Jovial Cheukam Ngouonou, Rémi Douence, Claude-Guy Quimper
- article
- CPAIOR 2023 - 20th International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research, May 2023, Nice, France. pp.378-394, ⟨10.1007/978-3-031-33271-5_25⟩
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Compositional pre-processing for automated reasoning in dependent type theory
- auteur
- Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial
- article
- CPP 2023 - Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- Pursuing Shtuck
- auteur
- Pierre-Marie Pédrot
- article
- 2023
- typdoc
- Preprints, Working Papers, ...
- Accès au texte intégral et bibtex
-
- titre
- Correct and Complete Type Checking and Certified Erasure for Coq, in Coq
- auteur
- Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter
- article
- 2023
- typdoc
- Preprints, Working Papers, ...
- Accès au texte intégral et bibtex
-
2022
Journal articles
- titre
- A Reasonably Gradual Type Theory
- auteur
- Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter
- article
- Proceedings of the ACM on Programming Languages, In press, ⟨10.1145/3547655⟩
- typdoc
- Journal articles
- Accès au texte intégral et bibtex
-
- titre
- The Advantages of Maintaining a Multitask, Project-Specific Bot: An Experience Report
- auteur
- Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert
- article
- IEEE Software, 2022, pp.2-7. ⟨10.1109/MS.2022.3179773⟩
- typdoc
- Journal articles
- Accès au texte intégral et bibtex
-
- titre
- Observational Equality: Now For Good
- auteur
- Loïc Pujet, Nicolas Tabareau
- article
- Proceedings of the ACM on Programming Languages, 2022, 6 (POPL), pp.1-29. ⟨10.1145/3498693⟩
- typdoc
- Journal articles
- Accès au texte intégral et bibtex
-
- titre
- Gradualizing the Calculus of Inductive Constructions
- auteur
- Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter
- article
- ACM Transactions on Programming Languages and Systems (TOPLAS), 2022, ⟨10.1145/3495528⟩
- typdoc
- Journal articles
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Efficient “out of heap” pointers for multicore OCaml
- auteur
- Guillaume Munch-Maccagnoni
- article
- OCaml 2022 - OCaml Users and Developers Workshop, Matija Pretnar, Sep 2022, Ljubljana, Slovenia. pp.1-7
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Boxroot, fast movable GC roots for a better FFI
- auteur
- Guillaume Munch-Maccagnoni, Gabriel Scherer
- article
- ML Family Workshop, Benoît Montagu, Sep 2022, Ljubljana, Slovenia
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Acquiring Maps of Interrelated Conjectures on Sharp Bounds
- auteur
- Nicolas Beldiceanu, Jovial Cheukam-Ngouonou, Rémi Douence, Ramiz Gindullin, Claude-Guy Quimper
- article
- CP 2022 - 28th International Conference on Principles and Practice of Constraint Programming, Jul 2022, Haifa, Israel. pp.1-18, ⟨10.4230/LIPIcs.CP.2022.6⟩
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Trakt : Uniformiser les types pour automatiser les preuves (démonstration)
- auteur
- Denis Cousineau, Enzo Crance, Assia Mahboubi
- article
- JFLA 2022 - 33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.261-263
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Gardening with the Pythia A model of continuity in a dependent setting
- auteur
- Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot
- article
- CSL 2022 - Computer Science Logic, Feb 2022, Göttingen, Germany. pp.1-19, ⟨10.4230/LIPIcs.CSL.2022.13⟩
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
2018
Lectures
- titre
- Calcul Formel et Preuves Formelles
- auteur
- Assia Mahboubi
- article
- Luminy, France. 2018, pp.1-10
- typdoc
- Lectures
- Accès au texte intégral et bibtex
-
2017
Conference papers
- titre
- Duploid situations in concurrent games
- auteur
- Pierre Clairambault, Guillaume Munch-Maccagnoni
- article
- 12th Workshop on Games for Logic and Programming Languages (GaLoP XII), Juha Kontinen, Marina Lenisa, Apr 2017, Uppsala, Sweden
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-