Publications
This list has been generated on 10 May 2023 from HAL and may be outdated.
You can check out our latest list of publications on HAL.
Showing 107 articles
Correct and Complete Type Checking and Certified Erasure for Coq, in Coq
Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter (2023)
Design patterns of hierarchies for order structures
Xavier Allamigeon, Quentin Canu, Cyril Cohen, Kazuhiko Sakaguchi, Pierre-Yves Strub (2023)
Deciding contextual equivalence of ν-calculus with effectful contexts (full version)
Daniel Hirschkoff, Guilhem Jaber, Enguerrand Prebet (2023)
Computing with Extensionality Principles in Type Theory, Calculer avec des Principes d'Extensionnalité en Théorie des Types
Loïc Pujet (2022)
Boxroot, fast movable GC roots for a better FFI
Guillaume Munch-Maccagnoni, Gabriel Scherer (2022)
ML Family Workshop
Efficient “out of heap” pointers for multicore OCaml
Guillaume Munch-Maccagnoni (2022)
OCaml 2022 - OCaml Users and Developers Workshop
Compositional pre-processing for automated reasoning in dependent type theory
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial (2023)
CPP 2023 - Certified Programs and Proofs
Duploid situations in concurrent games
Pierre Clairambault, Guillaume Munch-Maccagnoni (2017)
12th Workshop on Games for Logic and Programming Languages (GaLoP XII)
Constructive and Synthetic Reducibility Degrees: Post's Problem for Many-one and Truth-table Reducibility in Coq
Yannick Forster, Felix Jahn (2023)
CSL 2023 - 31st EACSL Annual Conference on Computer Science Logic
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory
Yannick Forster, Felix Jahn, Gert Smolka (2023)
CPP 2023 - 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
Parametric Church’s Thesis: Synthetic Computability Without Choice
Yannick Forster (2022)
Synthetic Kolmogorov Complexity in Coq
Yannick Forster, Fabian Kunze, Nils Lauermann (2022)
ITP 2022 - 13th International Conference on Interactive Theorem Proving
Impredicative Observational Equality
Loïc Pujet, Nicolas Tabareau (2023)
POPL 2023 - 50th ACM SIGPLAN Symposium on Principles of Programming Languages
Bidirectional Typing for the Calculus of Inductive Constructions, Typage Bidirectionnel pour le Calcul des Constructions Inductives
Meven Lennon-Bertrand (2022)
Acquiring Maps of Interrelated Conjectures on Sharp Bounds, Acquisition de cartes de conjectures interdépendantes sur les bornes précises
Nicolas Beldiceanu, Jovial Cheukam-Ngouonou, Rémi Douence, Ramiz Gindullin, Claude-Guy Quimper (2022)
CP 2022 - 28th International Conference on Principles and Practice of Constraint Programming
A Reasonably Gradual Type Theory
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter (2022)
Proceedings of the ACM on Programming Languages
The Advantages of Maintaining a Multitask, Project-Specific Bot: An Experience Report
Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert (2022)
IEEE Software
Trakt : Uniformiser les types pour automatiser les preuves (démonstration)
Denis Cousineau, Enzo Crance, Assia Mahboubi (2022)
JFLA 2022 - 33èmes Journées Francophones des Langages Applicatifs
For Finitary Induction-Induction, Induction is Enough
Ambrus Kaposi, András Kovács, Ambroise Lafont (2019)
TYPES 2019: 25th International Conference on Types for Proofs and Programs
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)
Yannick Forster, Felix Jahn, Gert Smolka (2022)
Probabilistic resource limits using StatMemprof
Guillaume Munch-Maccagnoni (2021)
OCaml 2021- OCaml Users and Developers Workshop
Temporal Refinements for Guarded Recursive Types
Guilhem Jaber, Colin Riba (2021)
ESOP 2021 - 30th European Symposium on Programming
A formal proof of the irrationality of ζ(3)
Assia Mahboubi, Thomas Sibut-Pinote (2021)
Logical Methods in Computer Science
Touring the MetaCoq Project (Invited Paper)
Matthieu Sozeau (2021)
LFMTP 2021 - Logical Frameworks and Meta-Languages: Theory and Practice
Types are internal infinity-groupoids
Eric Finster, Antoine Allioux, Matthieu Sozeau (2021)
LICS 2021
Theorems for free from separation logic specifications
Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos (2021)
Proceedings of the ACM on Programming Languages
Gardening with the Pythia A model of continuity in a dependent setting, Jardiner avec la Pythie
Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot (2022)
CSL 2022 - Computer Science Logic
Complete trace models of state and control
Guilhem Jaber, Andrzej S Murawski (2021)
ESOP 2021 - 30th European Symposium on Programming
Compositional relational reasoning via operational game semantics
Guilhem Jaber, Andrzej Murawski (2021)
LICS 2021 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science
Gradualizing the Calculus of Inductive Constructions
Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter (2022)
ACM Transactions on Programming Languages and Systems (TOPLAS)
Observational Equality: Now For Good
Loïc Pujet, Nicolas Tabareau (2022)
POPL 2022: Symposium on Principles of Programming Languages
Games, mobile processes, Dfunctions
Guilhem Jaber, Davide Sangiorgi (2022)
CSL 2022 - 30th EACSL Annual Conference on Computer Science Logic
The Multiverse: Logical Modularity for Proof Assistants
Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter (2021)
A type theory with definitional proof-irrelevance, Une théorie des types avec insignifiance des preuves définitionnelle
Gaëtan Gilbert (2019)
Unsolvability of the Quintic Formalized in Dependent Type Theory
Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub (2021)
ITP 2021 - 12th International Conference on Interactive Theorem Proving
Complete Bidirectional Typing for the Calculus of Inductive Constructions
Meven Lennon-Bertrand (2021)
ITP 2021 - 12th International Conference on Interactive Theorem Proving
Temporal Refinements for Guarded Recursive Types (full version)
Guilhem Jaber, Colin Riba (2021)
Towards better systems programming in OCaml with out-of-heap allocation
Guillaume Munch-Maccagnoni (2020)
ML Workshop 2020
The Marriage of Univalence and Parametricity
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau (2021)
Journal of the ACM (JACM)
Complete trace models of state and control (full version)
Guilhem Jaber, Andrzej S. Murawski (2021)
Machine-checked computer-aided mathematics
Assia Mahboubi (2021)
Model structure on the universe of all types in interval type theory
Simon Boulier, Nicolas Tabareau (2020)
Mathematical Structures in Computer Science
The Taming of the Rew: A Type Theory with Computational Assumptions
Jesper Cockx, Nicolas Tabareau, Théo Winterhalter (2021)
Proceedings of the ACM on Programming Languages
Modules over monads and operational semantics
André Hirschowitz, Tom Hirschowitz, Ambroise Lafont (2020)
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Russian Constructivism in a Prefascist Theory
Pierre-Marie Pédrot (2020)
LICS 2020 - Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science
Competing inheritance paths in dependent type theory: a case study in functional analysis
Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi (2020)
IJCAR 2020 - International Joint Conference on Automated Reasoning
Dependent Type Theory in Polarised Sequent Calculus (abstract)
Étienne Miquey, Xavier Montillet, Guillaume Munch-Maccagnoni (2020)
TYPES 2020 - 26th International Conference on Types for Proofs and Programs
Cubical Synthetic Homotopy Theory
Anders Mörtberg, Loïc Pujet (2020)
CPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs
Revisiting the duality of computation: an algebraic analysis of classical realizability models
Étienne Miquey (2020)
CSL 2020 - Conference on Computer Science Logic
SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References
Guilhem Jaber (2020)
Proceedings of the ACM on Programming Languages
Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter (2020)
Proceedings of the ACM on Programming Languages
Chiralités et exponentielles: un peu de différentiation
Esaïe Bauer, Marie Kerjean (2019)
The folk model category structure on strict $\omega$-categories is monoidal
Dimitri Ara, Maxime Lucas (2020)
Theory and Applications of Categories
The Diamond Lemma for non-terminating rewriting systems using deterministic reduction strategies
Cyrille Chenavier, Maxime Lucas (2019)
IWC 2019 - 8th International Workshop on Confluence
An implementation of polygraphs
Maxime Lucas (2019)
The Fire Triangle
Pierre-Marie Pédrot, Nicolas Tabareau (2020)
Proceedings of the ACM on Programming Languages
Reduction Monads and Their Signatures
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi (2020)
Proceedings of the ACM on Programming Languages
Heterogeneous Substitution Systems Revisited
Benedikt Ahrens, Ralph Matthes (2018)
CoqTL: A Coq DSL for Rule-Based Model Transformation
Zheng Cheng, Massimo Tisi, Rémi Douence (2020)
Software and Systems Modeling
Equivalences for Free
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau (2018)
Proceedings of the ACM on Programming Languages
Modular specification of monads through higher-order presentations
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi (2019)
FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction
Setoid type theory - a syntactic translation
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau (2019)
MPC 2019 - 13th International Conference on Mathematics of Program Construction
A Reasonably Exceptional Type Theory
Pierre-Marie Pédrot, Nicolas Tabareau, Hans Jacob Fehrmann, Éric Tanter (2019)
Proceedings of the ACM on Programming Languages
Efficient Deconstruction with Typed Pointer Reversal (abstract)
Guillaume Munch-Maccagnoni, Rémi Douence (2019)
ML 2019 - Workshop
A certificate-based approach to formally verified approximations
Florent Bréhard, Assia Mahboubi, Damien Pous (2019)
ITP 2019 - Tenth International Conference on Interactive Theorem Proving
The MetaCoq Project
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter (2020)
Journal of Automated Reasoning
A type-theoretical definition of weak ω-categories
Eric Finster, Samuel Mimram (2017)
LICS 2017 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science
Memory bijections: reasoning about exact memory transformations induced by refactorings in CompCert C
Igor Zhirkov, Julien Cohen, Rémi Douence (2019)
Extending type theory with syntactic models, Etendre la théorie des types à l'aide de modèles syntaxiques
Simon Pierre Boulier (2018)
A preview of a tutorial on L (polarized μμ-tilde)
Kenji Maillard, Étienne Miquey, Xavier Montillet, Guillaume Munch-Maccagnoni, Gabriel Scherer (2018)
HOPE 2018 - 7th ACM SIGPLAN Workshop on Higher-Order Programming with Effects
An explicit formula for the free exponential modality of linear logic
Paul-André Melliès, Nicolas Tabareau, Christine Tasson (2018)
Mathematical Structures in Computer Science
What term assignments can do for focusing
Guillaume Munch-Maccagnoni (2017)
4th International Workshop on Structures and Deduction (SD 2017)
Higher-order distributions for differential linear logic.
Marie Kerjean, Jean-Simon Lemay (2019)
Continuation-and-environment-passing style translations: a focus on call-by-need
Hugo Herbelin, Étienne Miquey (2019)
Functional description of sequence constraints and synthesis of combinatorial objects, Description fonctionnelle de contraintes sur des séquences et synthèse d’objets combinatoires
Ekaterina Arafailova (2018)
A sequent calculus with dependent types for classical arithmetic
Étienne Miquey (2018)
LICS 2018 - 33th Annual ACM/IEEE Symposium on Logic in Computer Science
The Coq Proof Assistant, version 8.8.0
The Coq Development Team (2018)
Goodwillie's calculus of functors and higher topos theory
Mathieu Anel, Georg Biedermann, Eric Finster, André Joyal (2018)
Journal of topology
Eliminating Reflection from Type Theory
Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau (2019)
CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs
High-level signatures and initial semantics
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi (2018)
27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
Preface: Special Issue on Homotopy Type Theory and Univalent Foundations
Peter Lefanu Lumsdaine, Nicolas Tabareau (2018)
Journal of Automated Reasoning
Definitional Proof-Irrelevance without K
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau (2019)
Proceedings of the ACM on Programming Languages
Static interpretation of higher-order modules in Futhark: functional GPU programming in the large
Martin Elsman, Troels Henriksen, Danil Annenkov, Cosmin Oancea (2018)
Proceedings of the ACM on Programming Languages
Certified Compilation of Financial Contracts
Danil Annenkov, Martin Elsman (2018)
PPDP '18 - 20th International Symposium on Principles and Practice of Declarative Programming
Global Constraint Catalog, Volume II, Time-Series Constraints
Ekaterina Arafailova, Nicolas Beldiceanu, Rémi Douence, Mats Carlsson, Pierre Flener, Justin Pearson, María Andreína Francisco Rodríguez, Helmut Simonis (2018)
The Abstract Accountability Language: its Syntax, Semantics and Tools
Walid Benghabrit, Hervé Grall, Jean-Claude Royer, Anderson Santana de Oliveira (2018)
Every λ-Term is Meaningful for the Infinitary Relational Model
Pierre Vial (2018)
LICS 2018 - Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science
Failure is Not an Option An Exceptional Type Theory
Pierre-Marie Pédrot, Nicolas Tabareau (2018)
ESOP 2018 - 27th European Symposium on Programming
Chemical foundations of distributed aspects
Nicolas Tabareau, Éric Tanter (2019)
Distributed Computing
Towards Certified Meta-Programming with Typed Template-Coq
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau (2018)
ITP 2018 - 9th Conference on Interactive Theorem Proving
A resource modality for RAII
Guillaume Combette, Guillaume Munch-Maccagnoni (2018)
LOLA 2018: Workshop on Syntax and Semantics of Low-Level Languages
A Classical Sequent Calculus with Dependent Types
Étienne Miquey (2019)
ACM Transactions on Programming Languages and Systems (TOPLAS)
A Classical Sequent Calculus with Dependent Types
Étienne Miquey (2018)
Formally Verified Approximations of Definite Integrals
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote (2019)
Journal of Automated Reasoning
Resource Polymorphism
Guillaume Munch-Maccagnoni (2018)
Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus With Control
Étienne Miquey, Hugo Herbelin (2018)
FOSSACS 18 - 21st International Conference on Foundations of Software Science and Computation Structures
Formalizing Implicative Algebras in Coq
Étienne Miquey (2018)
ITP 2018 - 9th International Conference on Interactive Theorem Proving
Typed Template Coq -- Certified Meta-Programming in Coq
Abhishek Anand, Simon Boulier, Nicolas Tabareau, Matthieu Sozeau (2018)
CoqPL 2018 - The Fourth International Workshop on Coq for Programming Languages
Foundations of Dependent Interoperability
Pierre-Evariste Dagand, Nicolas Tabareau, Éric Tanter (2018)
Journal of Functional Programming
Normalization by evaluation for sized dependent types
Andreas Abel, Andrea Vezzosi, Théo Winterhalter (2017)
Proceedings of the ACM on Programming Languages
Note on Curry's style for Linear Call-by-Push-Value
Guillaume Munch-Maccagnoni (2017)
Displayed Categories
Benedikt Ahrens, Peter Lefanu Lumsdaine (2017)
2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Categorical Structures for Type Theory in Univalent Foundations
Benedikt Ahrens, Peter Lefanu Lumsdaine, Vladimir Voevodsky (2017)
26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Note on models of polarised intuitionistic logic
Guillaume Munch-Maccagnoni (2017)
Théories géométriques pour l'algèbre des nombres réels
Henri Lombardi, Assia Mahboubi (2017)
Contemporary mathematics
The next 700 syntactical models of type theory
Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau (2017)
Certified Programs and Proofs (CPP 2017)
An Effectful Way to Eliminate Addiction to Dependence
Pierre-Marie Pédrot, Nicolas Tabareau (2017)
Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on