Publications HAL du labo/EPI 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
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
https://hal.science/hal-04360462/file/jfla2024-paper-5.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
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
https://inria.hal.science/hal-04407164/file/jfla2024-paper-sozeau.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
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
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
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
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
https://inria.hal.science/hal-04379245/file/abstractTypes.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
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
https://hal.science/hal-03955303/file/main.pdf 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
https://inria.hal.science/hal-03901942/file/forster_jahn_synthetic_reducibility_csl23.pdf 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
https://inria.hal.science/hal-03891390/file/myhill-cantor-cpp23.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

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
https://hal.science/hal-04225130/file/porting.pdf 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
https://theses.hal.science/tel-04335842/file/allioux-PhD-thesis-8.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
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
https://hal.science/hal-04160858/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
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
https://inria.hal.science/hal-04008820/file/relorder.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
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
https://inria.hal.science/hal-03596267/file/LIPIcs-ITP-2022-12%281%29.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
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
https://hal.science/hal-03407123/file/csl.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

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
https://arxiv.org/pdf/2112.11781 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
https://inria.hal.science/hal-04433492/file/Rapport_Stage.pdf BibTex

Theses

titre
Computing with Extensionality Principles in Type Theory
auteur
Loïc Pujet
article
Logic in Computer Science [cs.LO]. Nantes Université, 2022. English. ⟨NNT : ⟩
typdoc
Theses
Accès au bibtex
BibTex
titre
Bidirectional Typing for the Calculus of Inductive Constructions
auteur
Meven Lennon-Bertrand
article
Autre [cs.OH]. Nantes Université, 2022. Français. ⟨NNT : 2022NANU4033⟩
typdoc
Theses
Accès au texte intégral et bibtex
https://theses.hal.science/tel-03848595/file/LENNONBERTRAND.pdf 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
https://inria.hal.science/hal-03580081/file/fscd22-full.pdf BibTex

2021

Journal articles

titre
Theorems for free from separation logic specifications
auteur
Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos
article
Proceedings of the ACM on Programming Languages, 2021, 5 (ICFP), pp.1-29. ⟨10.1145/3473586⟩
typdoc
Journal articles
Accès au bibtex
BibTex
titre
A formal proof of the irrationality of ζ(3)
auteur
Assia Mahboubi, Thomas Sibut-Pinote
article
Logical Methods in Computer Science, 2021, 17 (1), pp.1-25. ⟨10.23638/LMCS-17(1:16)2021⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03517003/file/1912.06611.pdf BibTex
titre
The Marriage of Univalence and Parametricity
auteur
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
article
Journal of the ACM (JACM), 2021, 68 (1), pp.1-44. ⟨10.1145/3429979⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03120580/file/main_jacm.pdf BibTex
titre
The Taming of the Rew: A Type Theory with Computational Assumptions
auteur
Jesper Cockx, Nicolas Tabareau, Théo Winterhalter
article
Proceedings of the ACM on Programming Languages, 2021, POPL 2021, ⟨10.1145/3434341⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://hal.science/hal-02901011/file/main_popl.pdf BibTex

Conference papers

titre
Probabilistic resource limits using StatMemprof
auteur
Guillaume Munch-Maccagnoni
article
OCaml 2021- OCaml Users and Developers Workshop, Aug 2021, Online, France. pp.1-2
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03517592/file/memprof-limits-ocaml-workshop.pdf BibTex
titre
Touring the MetaCoq Project (Invited Paper)
auteur
Matthieu Sozeau
article
LFMTP 2021 - Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2021, Pittsburg, United States. pp.1-17
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03516619/file/Touring_the_MetaCoq_Project-LFMTP21.pdf BibTex
titre
Compositional relational reasoning via operational game semantics
auteur
Guilhem Jaber, Andrzej Murawski
article
LICS 2021 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2021, Rome, Italy. pp.1-13, ⟨10.1109/LICS52264.2021.9470524⟩
typdoc
Conference papers
Accès au bibtex
BibTex
titre
Complete Bidirectional Typing for the Calculus of Inductive Constructions
auteur
Meven Lennon-Bertrand
article
ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome, Italy. pp.1-19, ⟨10.4230/LIPIcs.ITP.2021.24⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.science/hal-03139924/file/main.pdf BibTex
titre
Unsolvability of the Quintic Formalized in Dependent Type Theory
auteur
Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub
article
ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome / Virtual, France
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03136002/file/main.pdf BibTex
titre
Types are internal infinity-groupoids
auteur
Eric Finster, Antoine Allioux, Matthieu Sozeau
article
LICS 2021, Jun 2021, Rome, Italy
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03133144/file/types-are-grpds-ext.pdf BibTex
titre
Temporal Refinements for Guarded Recursive Types
auteur
Guilhem Jaber, Colin Riba
article
ESOP 2021 - 30th European Symposium on Programming, Mar 2021, Luxembourg, Luxembourg. pp.548-578, ⟨10.1007/978-3-030-72019-3_20⟩
typdoc
Conference papers
Accès au bibtex
BibTex
titre
Complete trace models of state and control
auteur
Guilhem Jaber, Andrzej S Murawski
article
ESOP 2021 - 30th European Symposium on Programming, Mar 2021, Luxembourg, Luxembourg. pp.348-374, ⟨10.1007/978-3-030-72019-3_13⟩
typdoc
Conference papers
Accès au bibtex
https://arxiv.org/pdf/2101.08491 BibTex

Habilitation à diriger des recherches

titre
Machine-checked computer-aided mathematics
auteur
Assia Mahboubi
article
Logic in Computer Science [cs.LO]. Université de Nantes (UN), Nantes, FRA., 2021
typdoc
Habilitation à diriger des recherches
Accès au texte intégral et bibtex
https://theses.hal.science/tel-03107626/file/memoir_with_cover.pdf BibTex

Preprints, Working Papers, ...

titre
The Multiverse: Logical Modularity for Proof Assistants
auteur
Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter
article
2021
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03324596/file/main.pdf BibTex
titre
Complete trace models of state and control (full version)
auteur
Guilhem Jaber, Andrzej S. Murawski
article
2021
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://hal.science/hal-03116698/file/esop.pdf BibTex
titre
Temporal Refinements for Guarded Recursive Types (full version)
auteur
Guilhem Jaber, Colin Riba
article
2021
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://hal.science/hal-02512655/file/reftrees.pdf BibTex

2020

Journal articles

titre
Model structure on the universe of all types in interval type theory
auteur
Simon Boulier, Nicolas Tabareau
article
Mathematical Structures in Computer Science, 2020, pp.1-32. ⟨10.1017/S0960129520000213⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02966633/file/model_structure_on_the_universe_of_all_types_in_interval_type_theory.pdf BibTex
titre
The folk model category structure on strict $\omega$-categories is monoidal
auteur
Dimitri Ara, Maxime Lucas
article
Theory and Applications of Categories, 2020, 35 (21), pp.745-808
typdoc
Journal articles
Accès au bibtex
https://arxiv.org/pdf/1909.13564 BibTex
titre
The MetaCoq Project
auteur
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
article
Journal of Automated Reasoning, 2020, ⟨10.1007/s10817-019-09540-0⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02167423/file/The_MetaCoq_Project.pdf BibTex
titre
The Fire Triangle
auteur
Pierre-Marie Pédrot, Nicolas Tabareau
article
Proceedings of the ACM on Programming Languages, 2020, pp.1-28. ⟨10.1145/3371126⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://hal.science/hal-02383109/file/main.pdf BibTex
titre
Reduction Monads and Their Signatures
auteur
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
article
Proceedings of the ACM on Programming Languages, 2020, pp.1-29. ⟨10.1145/3371099⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02380682/file/main.pdf BibTex
titre
Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
auteur
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter
article
Proceedings of the ACM on Programming Languages, 2020, pp.1-28. ⟨10.1145/3371076⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://hal.science/hal-02380196/file/popl20main-p34-p-79d1b9f-43140-final.pdf BibTex
titre
CoqTL: A Coq DSL for Rule-Based Model Transformation
auteur
Zheng Cheng, Massimo Tisi, Rémi Douence
article
Software and Systems Modeling, 2020, 19, pp.425-439. ⟨10.1007/s10270-019-00765-6⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://hal.science/hal-02333564/file/Final.pdf BibTex
titre
SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References
auteur
Guilhem Jaber
article
Proceedings of the ACM on Programming Languages, In press, 28, pp.1-28. ⟨10.1145/3371127⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://hal.science/hal-02388621/file/popl20main-p219-p-a0fe6b0-43145-final.pdf BibTex

Conference papers

titre
Towards better systems programming in OCaml with out-of-heap allocation
auteur
Guillaume Munch-Maccagnoni
article
ML Workshop 2020, Aug 2020, Jersey City, United States. pp.1-6
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03142386/file/ml2020-paper8.pdf BibTex
titre
Russian Constructivism in a Prefascist Theory
auteur
Pierre-Marie Pédrot
article
LICS 2020 - Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken, Germany. pp.1-14, ⟨10.1145/3373718.3394740⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02548315/file/main.pdf BibTex
titre
Competing inheritance paths in dependent type theory: a case study in functional analysis
auteur
Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi
article
IJCAR 2020 - International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.1-19
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02463336/file/ijcar%20%281%29.pdf BibTex
titre
Dependent Type Theory in Polarised Sequent Calculus (abstract)
auteur
Étienne Miquey, Xavier Montillet, Guillaume Munch-Maccagnoni
article
TYPES 2020 - 26th International Conference on Types for Proofs and Programs, Mar 2020, Torino, Italy. pp.1-3
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02505671/file/ldep_types2020.pdf BibTex
titre
Cubical Synthetic Homotopy Theory
auteur
Anders Mörtberg, Loïc Pujet
article
CPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2020, New Orleans, United States. pp.1-14, ⟨10.1145/3372885.3373825⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.science/hal-02394145/file/main.pdf BibTex
titre
Revisiting the duality of computation: an algebraic analysis of classical realizability models
auteur
Étienne Miquey
article
CSL 2020 - Conference on Computer Science Logic, Jan 2020, Barcelone, Spain. pp.1-52, ⟨10.4230/LIPIcs.CSL.2020.30⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.science/hal-02305560/file/main.pdf BibTex
titre
Modules over monads and operational semantics
auteur
André Hirschowitz, Tom Hirschowitz, Ambroise Lafont
article
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), 2020, Paris, France. pp.12:1--12:23, ⟨10.4230/LIPIcs.FSCD.2020.12⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.science/hal-02338144/file/LIPIcs-FSCD-2020-12.pdf BibTex

2019

Journal articles

titre
A Reasonably Exceptional Type Theory
auteur
Pierre-Marie Pédrot, Nicolas Tabareau, Hans Jacob Fehrmann, Éric Tanter
article
Proceedings of the ACM on Programming Languages, 2019, Issue ICFP, 3, pp.1-29. ⟨10.1145/3341712⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02189128/file/icfp19main-p108-p-48a52d2-41764-final.pdf BibTex
titre
Chemical foundations of distributed aspects
auteur
Nicolas Tabareau, Éric Tanter
article
Distributed Computing, 2019, 32 (3), pp.193-216. ⟨10.1007/s00446-018-0334-6⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01811884/file/main.pdf BibTex
titre
A Classical Sequent Calculus with Dependent Types
auteur
Étienne Miquey
article
ACM Transactions on Programming Languages and Systems (TOPLAS), 2019, 41 (2), pp.1-48. ⟨10.1145/3230625⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01519929/file/dLtp.pdf BibTex
titre
Formally Verified Approximations of Definite Integrals
auteur
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
article
Journal of Automated Reasoning, 2019, 62 (2), pp.281-300. ⟨10.1007/s10817-018-9463-7⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01630143/file/main.pdf BibTex
titre
Definitional Proof-Irrelevance without K
auteur
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau
article
Proceedings of the ACM on Programming Languages, 2019, POPL'19, pp.1-28. ⟨10.1145/329031610.1145/3290316⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01859964/file/main_popl.pdf BibTex

Conference papers

titre
Setoid type theory - a syntactic translation
auteur
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau
article
MPC 2019 - 13th International Conference on Mathematics of Program Construction, Oct 2019, Porto, Portugal. pp.155-196, ⟨10.1007/978-3-030-33636-3_7⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02281225/file/mpc2019.pdf BibTex
titre
A certificate-based approach to formally verified approximations
auteur
Florent Bréhard, Assia Mahboubi, Damien Pous
article
ITP 2019 - Tenth International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.1-19, ⟨10.4230/LIPIcs.ITP.2019.8⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://laas.hal.science/hal-02088529/file/chebapprox.pdf BibTex
titre
Efficient Deconstruction with Typed Pointer Reversal (abstract)
auteur
Guillaume Munch-Maccagnoni, Rémi Douence
article
ML 2019 - Workshop, KC Sivaramakrishnan, Aug 2019, Berlin, Germany. pp.1-8
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02177326/file/efficient-drops-mlworkshop.pdf BibTex
titre
The Diamond Lemma for non-terminating rewriting systems using deterministic reduction strategies
auteur
Cyrille Chenavier, Maxime Lucas
article
IWC 2019 - 8th International Workshop on Confluence, Jun 2019, Dortmund, Germany. pp.1-5
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.science/hal-02385139/file/Source.pdf BibTex
titre
Modular specification of monads through higher-order presentations
auteur
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
article
FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. pp.1-16, ⟨10.4230/LIPIcs.FSCD.2019.6⟩
typdoc
Conference papers
Accès au bibtex
https://arxiv.org/pdf/1903.00922 BibTex
titre
For Finitary Induction-Induction, Induction is Enough
auteur
Ambrus Kaposi, András Kovács, Ambroise Lafont
article
TYPES 2019: 25th International Conference on Types for Proofs and Programs, Jun 2019, Oslo, Norway. pp.6:1-6:30, ⟨10.4230/LIPIcs.TYPES.2019.6⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://imt-atlantique.hal.science/hal-03594037/file/paper.pdf BibTex
titre
Eliminating Reflection from Type Theory
auteur
Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau
article
CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Lisbonne, Portugal. pp.91-103, ⟨10.1145/3293880.3294095⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.science/hal-01849166/file/cpp19.pdf BibTex
titre
Higher-order distributions for differential linear logic.
auteur
Marie Kerjean, Jean-Simon Lemay
article
Foundations of Software Science and Computation Structures - 22nd International Conference, {FOSSACS} 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Mikolaj Bojanczyk and Alex Simpson, 2019, Prague (Czech Republic), Czech Republic. ⟨10.1007/978-3-030-17127-8\_19⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01969262/file/Higher-order-iso.pdf BibTex

Reports

titre
Memory bijections: reasoning about exact memory transformations induced by refactorings in CompCert C
auteur
Igor Zhirkov, Julien Cohen, Rémi Douence
article
[Research Report] LS2N, Université de Nantes. 2019
typdoc
Reports
Accès au texte intégral et bibtex
https://hal.science/hal-02078356/file/memory-bijection-report.pdf BibTex

Theses

titre
A type theory with definitional proof-irrelevance
auteur
Gaëtan Gilbert
article
Logic in Computer Science [cs.LO]. Ecole nationale supérieure Mines-Télécom Atlantique, 2019. English. ⟨NNT : 2019IMTA0169⟩
typdoc
Theses
Accès au texte intégral et bibtex
https://theses.hal.science/tel-03236271/file/2019IMTA0169_Gilbert-Gaetan.pdf BibTex

Preprints, Working Papers, ...

titre
Chiralités et exponentielles: un peu de différentiation
auteur
Esaïe Bauer, Marie Kerjean
article
2019
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02320704/file/article_HAL.pdf BibTex
titre
Continuation-and-environment-passing style translations: a focus on call-by-need
auteur
Hugo Herbelin, Étienne Miquey
article
2019
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01972846/file/esop19.pdf BibTex
titre
An implementation of polygraphs
auteur
Maxime Lucas
article
2019
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://hal.science/hal-02385110/file/poly.pdf BibTex

2018

Journal articles

titre
Goodwillie's calculus of functors and higher topos theory
auteur
Mathieu Anel, Georg Biedermann, Eric Finster, André Joyal
article
Journal of topology, 2018, 11 (4), pp.1100-1132. ⟨10.1112/topo.12082⟩
typdoc
Journal articles
Accès au bibtex
BibTex
titre
Preface: Special Issue on Homotopy Type Theory and Univalent Foundations
auteur
Peter Lefanu Lumsdaine, Nicolas Tabareau
article
Journal of Automated Reasoning, 2018, ⟨10.1007/s10817-018-9491-3⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01929871/file/main.pdf BibTex
titre
Equivalences for Free
auteur
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
article
Proceedings of the ACM on Programming Languages, 2018, ICFP'18, 2 (ICFP), pp.1-29. ⟨10.1145/3234615⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01559073/file/main_icfp.pdf BibTex
titre
Static interpretation of higher-order modules in Futhark: functional GPU programming in the large
auteur
Martin Elsman, Troels Henriksen, Danil Annenkov, Cosmin Oancea
article
Proceedings of the ACM on Programming Languages, 2018, 2 (ICFP), pp.97:1--97:30. ⟨10.1145/3236792⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01883524/file/ICFP18-modules.pdf BibTex
titre
An explicit formula for the free exponential modality of linear logic
auteur
Paul-André Melliès, Nicolas Tabareau, Christine Tasson
article
Mathematical Structures in Computer Science, 2018, 28 (7), pp.1253-1286. ⟨10.1017/S0960129516000426⟩
typdoc
Journal articles
Accès au bibtex
BibTex
titre
Foundations of Dependent Interoperability
auteur
Pierre-Evariste Dagand, Nicolas Tabareau, Éric Tanter
article
Journal of Functional Programming, 2018, 28, ⟨10.1017/S0956796818000011⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01629909/file/main.pdf BibTex

Conference papers

titre
A preview of a tutorial on L (polarized μμ-tilde)
auteur
Kenji Maillard, Étienne Miquey, Xavier Montillet, Guillaume Munch-Maccagnoni, Gabriel Scherer
article
HOPE 2018 - 7th ACM SIGPLAN Workshop on Higher-Order Programming with Effects, Sep 2018, St. Louis, United States
typdoc
Conference papers
Accès au bibtex
BibTex
titre
High-level signatures and initial semantics
auteur
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
article
27th EACSL Annual Conference on Computer Science Logic (CSL 2018), Sep 2018, Birmingham, United Kingdom. pp.1-20, ⟨10.4230/LIPIcs.CSL.2018.4⟩
typdoc
Conference papers
Accès au bibtex
https://arxiv.org/pdf/1805.03740 BibTex
titre
Certified Compilation of Financial Contracts
auteur
Danil Annenkov, Martin Elsman
article
PPDP '18 - 20th International Symposium on Principles and Practice of Declarative Programming, Sep 2018, Frankfurt am Main, Germany. pp.1-13, ⟨10.1145/3236950.3236955⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01883559/file/PPDP18-cert-comp-fin.pdf BibTex
titre
Formalizing Implicative Algebras in Coq
auteur
Étienne Miquey
article
ITP 2018 - 9th International Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. pp.459-476, ⟨10.1007/978-3-319-94821-8_27⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01703524/file/impalg.pdf BibTex
titre
Towards Certified Meta-Programming with Typed Template-Coq
auteur
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau
article
ITP 2018 - 9th Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. pp.20-39, ⟨10.1007/978-3-319-94821-8_2⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.science/hal-01809681/file/paper_39.pdf BibTex
titre
Every λ-Term is Meaningful for the Infinitary Relational Model
auteur
Pierre Vial
article
LICS 2018 - Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science, ACM, Jul 2018, Oxford, United Kingdom. pp.1-26
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.science/hal-01840744/file/hal-inf-rel-mod-conf.pdf BibTex
titre
A sequent calculus with dependent types for classical arithmetic
auteur
Étienne Miquey
article
LICS 2018 - 33th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford, United Kingdom. pp.720-729, ⟨10.1145/3209108.3209199⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01703526/file/dlpaw.pdf BibTex
titre
A resource modality for RAII
auteur
Guillaume Combette, Guillaume Munch-Maccagnoni
article
LOLA 2018: Workshop on Syntax and Semantics of Low-Level Languages, Jul 2018, Oxford, United Kingdom. pp.1-4
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01806634/file/raii-modality-short.pdf BibTex
titre
Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus With Control
auteur
Étienne Miquey, Hugo Herbelin
article
FOSSACS 18 - 21st International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessalonique, Greece. pp.276-292, ⟨10.1007/978-3-319-89366-2_15⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01624839/file/cbncps.pdf BibTex
titre
Failure is Not an Option An Exceptional Type Theory
auteur
Pierre-Marie Pédrot, Nicolas Tabareau
article
ESOP 2018 - 27th European Symposium on Programming, Apr 2018, Thessaloniki, Greece. pp.245-271, ⟨10.1007/978-3-319-89884-1_9⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01840643/file/main.pdf BibTex
titre
Typed Template Coq -- Certified Meta-Programming in Coq
auteur
Abhishek Anand, Simon Boulier, Nicolas Tabareau, Matthieu Sozeau
article
CoqPL 2018 - The Fourth International Workshop on Coq for Programming Languages, Jan 2018, Los Angeles, CA, United States. pp.1-2
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01671948/file/Anand-Boulier-Tabareau-Sozeau-CoqPL18.pdf BibTex

Book sections

titre
Heterogeneous Substitution Systems Revisited
auteur
Benedikt Ahrens, Ralph Matthes
article
Tarmo Uustalu. 21st International Conference on Types for Proofs and Programs (TYPES 2015), 69, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp.2:1-2:23, 2018, Leibniz International Proceedings in Informatics (LIPIcs), 978-3-95977-030-9. ⟨10.4230/LIPIcs.TYPES.2015.2⟩
typdoc
Book sections
Accès au texte intégral et bibtex
https://hal.science/hal-02360681/file/AhrensMatthes-HetSubstSysRevisited-TYPES2015-LIPIcs-Postproc.pdf BibTex

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

Reports

titre
Global Constraint Catalog, Volume II, Time-Series Constraints
auteur
Ekaterina Arafailova, Nicolas Beldiceanu, Rémi Douence, Mats Carlsson, Pierre Flener, Justin Pearson, María Andreína Francisco Rodríguez, Helmut Simonis
article
[Technical Report] IMT Atlantique. 2018, pp.1-3762
typdoc
Reports
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01374721/file/1609.08925v2.pdf BibTex
titre
The Abstract Accountability Language: its Syntax, Semantics and Tools
auteur
Walid Benghabrit, Hervé Grall, Jean-Claude Royer, Anderson Santana de Oliveira
article
[Research Report] IMT Atlantique. 2018
typdoc
Reports
Accès au texte intégral et bibtex
https://hal.science/hal-01856329/file/main.pdf BibTex

Software

titre
The Coq Proof Assistant, version 8.8.0
auteur
The Coq Development Team
article
2018
typdoc
Software
Accès au bibtex
BibTex

Theses

titre
Extending type theory with syntactic models
auteur
Simon Pierre Boulier
article
Logic in Computer Science [cs.LO]. Ecole nationale supérieure Mines-Télécom Atlantique, 2018. English. ⟨NNT : 2018IMTA0110⟩
typdoc
Theses
Accès au texte intégral et bibtex
https://theses.hal.science/tel-02007839/file/2018IMTA0110_Boulier-Simon.pdf BibTex
titre
Functional description of sequence constraints and synthesis of combinatorial objects
auteur
Ekaterina Arafailova
article
Discrete Mathematics [cs.DM]. Ecole nationale supérieure Mines-Télécom Atlantique, 2018. English. ⟨NNT : 2018IMTA0089⟩
typdoc
Theses
Accès au texte intégral et bibtex
https://theses.hal.science/tel-01962957/file/2018IMTA0089-Arafailova_Ekaterina.pdf BibTex

Preprints, Working Papers, ...

titre
A Classical Sequent Calculus with Dependent Types
auteur
Étienne Miquey
article
2018
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://hal.science/hal-01744359/file/dL-extended.pdf BibTex
titre
Resource Polymorphism
auteur
Guillaume Munch-Maccagnoni
article
2018
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01724997/file/ocaml-raii.pdf BibTex

2017

Journal articles

titre
Normalization by evaluation for sized dependent types
auteur
Andreas Abel, Andrea Vezzosi, Théo Winterhalter
article
Proceedings of the ACM on Programming Languages, 2017, 1, pp.33. ⟨10.1145/3110277⟩
typdoc
Journal articles
Accès au texte intégral et bibtex
https://hal.science/hal-01596179/file/icfp17-main84.pdf BibTex
titre
Théories géométriques pour l'algèbre des nombres réels
auteur
Henri Lombardi, Assia Mahboubi
article
Contemporary mathematics, 2017, Ordered algebraic structures and related topics, 697, pp.239--264
typdoc
Journal articles
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01426164/file/Reels-geom-court.pdf BibTex

Conference papers

titre
What term assignments can do for focusing
auteur
Guillaume Munch-Maccagnoni
article
4th International Workshop on Structures and Deduction (SD 2017), Sep 2017, Oxford, United Kingdom
typdoc
Conference papers
Accès au bibtex
BibTex
titre
Displayed Categories
auteur
Benedikt Ahrens, Peter Lefanu Lumsdaine
article
2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Sep 2017, Oxford, United Kingdom. ⟨10.4230/LIPIcs.FSCD.2017.5⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01584770/file/LIPIcs-FSCD-2017-5.pdf BibTex
titre
Categorical Structures for Type Theory in Univalent Foundations
auteur
Benedikt Ahrens, Peter Lefanu Lumsdaine, Vladimir Voevodsky
article
26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Aug 2017, Stockholm, Sweden. pp.8:1 - 8:16, ⟨10.4230/LIPIcs.CSL.2017.8⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01579271/file/LIPIcs-CSL-2017-8.pdf BibTex
titre
An Effectful Way to Eliminate Addiction to Dependence
auteur
Pierre-Marie Pédrot, Nicolas Tabareau
article
Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on, Jun 2017, Reykjavik, Iceland. pp.12, ⟨10.1109/LICS.2017.8005113⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01441829/file/main.pdf BibTex
titre
A type-theoretical definition of weak ω-categories
auteur
Eric Finster, Samuel Mimram
article
LICS 2017 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. pp.1-12, ⟨10.1109/LICS.2017.8005124⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02154846/file/mimram_catt.pdf BibTex
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
titre
The next 700 syntactical models of type theory
auteur
Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau
article
Certified Programs and Proofs (CPP 2017), Jan 2017, Paris, France. pp.182 - 194, ⟨10.1145/3018610.3018620⟩
typdoc
Conference papers
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01445835/file/main.pdf BibTex

Preprints, Working Papers, ...

titre
Note on models of polarised intuitionistic logic
auteur
Guillaume Munch-Maccagnoni
article
2017
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01540760/file/ll-cbpv.pdf BibTex
titre
Note on Curry's style for Linear Call-by-Push-Value
auteur
Guillaume Munch-Maccagnoni
article
2017
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01528857/file/curry.pdf BibTex