2024
Conference papers
- 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
- Towards a linear functional translation for borrowing
- auteur
- Sidney Congard
- 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
-
- titre
- Modular efficient deconstruction with typed pointer reversal
- auteur
- Jean Caspar, Guillaume Munch-Maccagnoni
- article
- JFLA 2024 - 35es Journées Francophones des Langages Applicatifs, Jan 2024, Saint-Jacut-de-la-Mer, France. pp.1-10
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- MetaCoq : de la métaprogrammation à l'extraction certifiée pour Coq
- auteur
- Matthieu Sozeau
- 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
- The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
- auteur
- Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter
- article
- 2024
- typdoc
- Preprints, Working Papers, ...
- Accès au texte intégral et bibtex
-
- 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
- Engineering logical relations for MLTT in Coq
- auteur
- Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Loïc Pujet
- 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
- Deciding contextual equivalence of ν-calculus with effectful contexts (full version)
- auteur
- Daniel Hirschkoff, Guilhem Jaber, Enguerrand Prebet
- article
- Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023., Apr 2023, Paris, France
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Constructive and Synthetic Reducibility Degrees: Post's Problem for Many-one and Truth-table Reducibility in Coq
- auteur
- Yannick Forster, Felix Jahn
- article
- CSL 2023 - 31st EACSL Annual Conference on Computer Science Logic, Feb 2023, Warsaw, Poland. pp.1-21, ⟨10.4230/LIPIcs.CSL.2023.16⟩
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory
- auteur
- Yannick Forster, Felix Jahn, Gert Smolka
- article
- CPP 2023 - 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-8, ⟨10.1145/3573105.3575690⟩
- 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
-
Reports
- titre
- Porting Coq Scripts to the Mathematical Components Library Version 2
- auteur
- Reynald Affeldt, Yves Bertot, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi
- article
- Inria Sophia Antipolis - Méditerranée, Université Côte d'Azur; National Institute of Advanced Industrial Science and Technology (AIST), Japan; ONERA / DTIS, Université de Toulouse, France. 2023, pp.1-12
- typdoc
- Reports
- Accès au texte intégral et bibtex
-
Theses
- titre
- Higher Structures in Homotopy Type Theory
- auteur
- Antoine Allioux
- article
- Computer Science [cs]. Université Paris Cité, 2023. English. ⟨NNT : ⟩
- typdoc
- Theses
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- Verified Extraction from Coq to OCaml
- auteur
- Yannick Forster, Matthieu Sozeau, Nicolas Tabareau
- article
- 2023
- typdoc
- Preprints, Working Papers, ...
- Accès au texte intégral et bibtex
-
- titre
- Definitional Functoriality for Dependent (Sub)Types
- auteur
- Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard
- article
- 2023
- typdoc
- Preprints, Working Papers, ...
- Accès au texte intégral et bibtex
-
- 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
-
- titre
- Design patterns of hierarchies for order structures
- auteur
- Xavier Allamigeon, Quentin Canu, Cyril Cohen, Kazuhiko Sakaguchi, Pierre-Yves Strub
- 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
- 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
- Synthetic Kolmogorov Complexity in Coq
- auteur
- Yannick Forster, Fabian Kunze, Nils Lauermann
- article
- ITP 2022 - 13th International Conference on Interactive Theorem Proving, Aug 2022, Haifa, Israel
- 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
- Games, mobile processes, Dfunctions
- auteur
- Guilhem Jaber, Davide Sangiorgi
- article
- CSL 2022 - 30th EACSL Annual Conference on Computer Science Logic, Feb 2022, Göttingen, Germany. pp.1-35
- 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
-
Book sections
- titre
- Parametric Church’s Thesis: Synthetic Computability Without Choice
- auteur
- Yannick Forster
- article
- Logical Foundations of Computer Science, 13137, Springer International Publishing, pp.70-89, 2022, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-93100-1_6⟩
- typdoc
- Book sections
- Accès au bibtex
-
Reports
- titre
- Formalisation et implémentation des propositions strictes dans MetaCoq
- auteur
- Yann Leray
- article
- Inria Rennes - Bretagne Atlantique; LS2N-Nantes Université. 2022, pp.17
- typdoc
- Reports
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- A Constructive and Synthetic Theory of Reducibility: Myhill's Isomorphism Theorem and Post's Problem for Many-one and Truth-table Reducibility in Coq (Full Version)
- auteur
- Yannick Forster, Felix Jahn, Gert Smolka
- article
- 2022
- typdoc
- Preprints, Working 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
-