Publications HAL de Simon,Boulier;Théo,Winterhalter;Xavier,Montillet;Ambroise,Lafont;Gaëtan,Gilbert;Igor,Zhirkov;Eric,Finster;Pierre,Vial;Etienne,Miquey;Danil,Annenkov;Julien,Cohen;Guillaume,Munch-Maccagnoni;Hervé,Graal;Rémi,Douence;Assia,Mahboubi;Nicolas,Tabareau;Kevin,Quirin;Pierre-Marie,Pédrot;Benedikt,Ahrens de la structure Gallinette

2024

Conference papers

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
https://hal.science/hal-04535982/file/main.pdf 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
https://hal.science/hal-04177913/file/main.pdf 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
https://hal.science/hal-04460576/file/Decompositions_AAAI__24%20%281%29.pdf 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
https://hal.science/hal-04266479/file/main.pdf 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
https://inria.hal.science/hal-04406342/file/jfla2024-paper-13.pdf 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
https://inria.hal.science/hal-04511667/file/RewriteRules.pdf 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
https://hal.science/hal-04214008/file/main.pdf 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
https://inria.hal.science/hal-04471683/file/main.pdf 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
https://hal.science/hal-04273257/file/2021-397.pdf 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
https://hal.science/hal-03857705/file/main.pdf 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
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
https://inria.hal.science/hal-04403667/file/abstract.pdf 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
https://inria.hal.science/hal-04378939/file/main.pdf 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
https://inria.hal.science/hal-04172297/file/article.pdf 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
https://hal.science/hal-04460561/file/CPAIOR_2023.pdf 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
https://inria.hal.science/hal-03901019/file/main.pdf 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
https://inria.hal.science/hal-04329663/file/main.pdf BibTex
titre
Pursuing Shtuck
auteur
Pierre-Marie Pédrot
article
2023
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04251754/file/main.pdf 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
https://inria.hal.science/hal-04077552/file/main%20%281%29.pdf 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
https://inria.hal.science/hal-03596652/file/main.pdf 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
https://inria.hal.science/hal-03479327/file/paper.pdf 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
https://inria.hal.science/hal-03367052/file/main.pdf 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
https://hal.science/hal-02896776/file/main.pdf 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
https://inria.hal.science/hal-03910312/file/large-pages-ocamlworkshop.pdf 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
https://inria.hal.science/hal-03910313/file/boxroot-mlworkshop.pdf 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
https://hal.science/hal-03789045/file/LIPIcs-CP-2022-6.pdf 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
https://inria.hal.science/hal-03626851/file/jfla22_paper_9.pdf 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
https://inria.hal.science/hal-03510671/file/gardening_with_the_pythia.pdf 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
https://hal.science/hal-04116824/file/CCIRM_2018__6_1_A2_0.pdf 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
https://inria.hal.science/hal-01991555/file/expo-galop-full.pdf BibTex