Publications
This list has been generated on 19 May 2025 from HAL and may be outdated.
You can check out our latest list of publications on HAL.
Showing 145 articles
Continuity in Type Theory, Continuité en théorie des types
Martin Baillon (2023)
Mathematical Components Analysis
Reynald Affeldt, Yves Bertot, Alessandro Bruni, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Pierre Roux, Kazuhiko Sakaguchi, Zachary Stone, Pierre-Yves Strub, Laurent Théry (2025)
Trocq
Cyril Cohen, Enzo Crance, Assia Mahboubi (2025)
A Zoo of Continuity Properties in Constructive Type Theory
Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot, Matthieu Piquerez (2025)
Classical notions of computation and the Hasegawa-Thielecke theorem
Éléonore Mangel, Paul-André Melliès, Guillaume Munch-Maccagnoni (2025)
Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting
Thiago Felicissimo, Jean-Pierre Jouannaud (2025)
Automated Proof Tactics for Model Transformation
Julien Cohen, Massimo Tisi, Rémi Douence (2024)
ECMFA 2024 - 20th European Conference on Modelling Foundations and Applications
Designing interrupts for ML and OCaml
Guillaume Munch-Maccagnoni, Leo White, Stephen Dolan (2024)
ML 2024 - ACM SIGPLAN Workshop on ML Family Workshop Higher-order, Typed, Inferred, Strict
Machine-Checked Categorical Diagrammatic Reasoning
Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez (2024)
9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
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 (2024)
Journal of the ACM (JACM)
All Your Base Are Belong to Us
Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter (2025)
Proceedings of the ACM on Programming Languages
Méta-programmation pour le transfert de preuve en théorie des types dépendants, Meta-Programming for Proof Transfer in Dependent Type Theory
Enzo Crance (2023)
Geometric theories for real number algebra without sign test or dependent choice axiom
Henri Lombardi, Assia Mahboubi (2024)
CCC 2024 - Continuity, Computability, Constructivity From Logic to Algorithms
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter (2024)
International Conference on Interactive Theorem Proving (ITP 2024)
Gradual Indexed Inductive Types
Mara Malewski, Kenji Maillard, Nicolas Tabareau, Éric Tanter (2024)
Proceedings of the ACM on Programming Languages
Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence
Cyril Cohen, Enzo Crance, Assia Mahboubi (2024)
ESOP 2024 - 33rd European Symposium on Programming
Temporal Refinements for Guarded Recursive Types
Guilhem Jaber, Colin Riba (2021)
ESOP 2021 - 30th European Symposium on Programming
$\partial$ is for Dialectica
Marie Kerjean, Pierre-Marie Pédrot (2024)
LICS 2024 - 39th Annual ACM/IEEE Symposium on Logic in Computer Science
Upon This Quote I Will Build My Church Thesis
Pierre-Marie Pédrot (2024)
LICS 2024 - 39th Annual ACM/IEEE Symposium on Logic in Computer Science
Definitional Functoriality for Dependent (Sub)Types
Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard (2023)
Observational Equality Meets CIC
Loïc Pujet, Nicolas Tabareau (2024)
ESOP 2024 - 33rd European Symposium on Programming
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
Composing Biases by Using CP to Decompose Minimal Functional Dependencies for Acquiring Complex Formulae
Ramiz Gindullin, Nicolas Beldiceanu, Jovial Cheukam-Ngouonou, Rémi Douence, Claude-Guy Quimper (2024)
AAAI 2024: 38th Annual AAAI Conference on Artificial Intelligence
Boolean-Arithmetic Equations: Acquisition and Uses
R Gindullin, Nicolas Beldiceanu, Jovial Cheukam Ngouonou, Rémi Douence, Claude-Guy Quimper (2023)
CPAIOR 2023: 20th International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research
Formalisation et implémentation des propositions strictes dans MetaCoq
Yann Leray (2022)
Trocq: Proof Transfer for Free, With or Without Univalence
Cyril Cohen, Enzo Crance, Assia Mahboubi (2024)
ESOP 2024 - 33rd European Symposium on Programming
MetaCoq : de la métaprogrammation à l'extraction certifiée pour Coq
Matthieu Sozeau (2024)
35es Journées Francophones des Langages Applicatifs (JFLA 2024)
Towards a linear functional translation for borrowing
Sidney Congard (2024)
35es Journées Francophones des Langages Applicatifs (JFLA 2024)
Modular efficient deconstruction with typed pointer reversal
Jean Caspar, Guillaume Munch-Maccagnoni (2024)
35es Journées Francophones des Langages Applicatifs (JFLA 2024)
The Rewster: The Coq Proof Assistant with Rewrite Rules
Gaëtan Gilbert, Yann Leray, Nicolas Tabareau, Théo Winterhalter (2023)
TYPES 2023 - 29th International Conference on Types for Proofs and Programs
Martin-Löf à la Coq
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet (2024)
CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs
Engineering logical relations for MLTT in Coq
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Loïc Pujet (2023)
TYPES 2023 - 29th International Conference on Types for Proofs and Programs
From Lost to the River: Embracing Sort Proliferation
Gaëtan Gilbert, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau (2023)
TYPES 2023 - 29th International Conference on Types for Proofs and Programs
Resource polymorphism: proposal for integrating first-class resources into ML
Guillaume Munch-Maccagnoni (2023)
Higher-order, Typed, Inferred, Strict: ML Family Workshop 2023
Verified Extraction from Coq to OCaml
Yannick Forster, Matthieu Sozeau, Nicolas Tabareau (2024)
Proceedings of the ACM on Programming Languages
A First Order Theory of Diagram Chasing, Une théorie du premier ordre pour la chasse au diagramme
Assia Mahboubi, Matthieu Piquerez (2024)
CSL 2024 - 32nd EACSL Annual Conference on Computer Science Logic
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
Philipp Haselwarter, Exequiel Rivas, Antoine van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Cătălin Hriţcu, Kenji Maillard, Bas Spitters (2023)
ACM Transactions on Programming Languages and Systems (TOPLAS)
Pursuing Shtuck
Pierre-Marie Pédrot (2023)
Porting Coq Scripts to the Mathematical Components Library Version 2
Reynald Affeldt, Yves Bertot, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi (2023)
Manifest Termination
Assia Mahboubi, Guillaume Melquiond (2023)
TYPES 2023 - 29th International Conference on Types for Proofs and Programs
Calcul Formel et Preuves Formelles
Assia Mahboubi (2018)
Journées nationales de calcul formel
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)
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.
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
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)
Proceedings of the ACM on 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
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)
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
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