Publications
This list has been generated on 14 October 2020 from HAL and may be outdated.
You can check out our latest list of publications on HAL.
Showing 67 articles
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 (2020)
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)
Gradualizing the Calculus of Inductive Constructions
Meven Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter (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
Chiralities in topological vector spaces
Marie Kerjean (2020)
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 (2019)
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 (2019)
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 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)
Duploid situations in concurrent games
Pierre Clairambault, Guillaume Munch-Maccagnoni (2017)
Games for Logic and Programming Languages XII (GaLoP)
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)
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 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)
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