2024
Journal articles
- 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
- Journal of the ACM (JACM), 2024, ⟨https://doi.org/10.1145/3706056⟩
- typdoc
- Journal articles
- Accès au texte intégral et bibtex
-
- titre
- Gradual Indexed Inductive Types
- auteur
- Mara Malewski, Kenji Maillard, Nicolas Tabareau, Éric Tanter
- article
- Proceedings of the ACM on Programming Languages, 2024, 8 (ICFP), pp.544-572. ⟨10.1145/3674644⟩
- typdoc
- Journal articles
- Accès au bibtex
-
- titre
- Verified Extraction from Coq to OCaml
- auteur
- Yannick Forster, Matthieu Sozeau, Nicolas Tabareau
- article
- Proceedings of the ACM on Programming Languages, 2024, 8 (PLDI), pp.52-75. ⟨10.1145/3656379⟩
- typdoc
- Journal articles
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Geometric theories for real number algebra without sign test or dependent choice axiom
- auteur
- Henri Lombardi, Assia Mahboubi
- article
- CCC 2024 - Continuity, Computability, Constructivity From Logic to Algorithms, Sep 2024, Nice, France. pp.1-152
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
- auteur
- Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter
- article
- International Conference on Interactive Theorem Proving (ITP 2024), Yves Bertot; Temur Kutsia; Michael Norrish, Sep 2024, Tbilisi, Georgia. pp.18, ⟨10.4230/LIPIcs.ITP.2024.26⟩
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- $\partial$ is for Dialectica
- auteur
- Marie Kerjean, Pierre-Marie Pédrot
- article
- LICS 2024 - 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2024, Tallinn, Estonia. pp.1-13
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- titre
- Upon This Quote I Will Build My Church Thesis
- auteur
- Pierre-Marie Pédrot
- article
- LICS 2024 - 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2024, Tallin, Estonia. pp.1-12, ⟨10.1145/3661814.3662070⟩
- typdoc
- Conference papers
- Accès au texte intégral et bibtex
-
- 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
-
- 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
-
- titre
- Artifact Report: 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.269-274, ⟨10.1007/978-3-031-57262-3_11⟩
- typdoc
- Conference papers
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- titre
- Modular efficient deconstruction with typed pointer reversal
- auteur
- Jean Caspar, Guillaume Munch-Maccagnoni
- 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
-
- 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
-
Preprints, Working Papers, ...
- 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
-
- 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
-
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
-
- 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
-
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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
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
-
Theses
- titre
- Continuity in Type Theory
- auteur
- Martin Baillon
- article
- Logic in Computer Science [cs.LO]. Nantes Université, 2023. English. ⟨NNT : ⟩
- typdoc
- Theses
- Accès au texte intégral et bibtex
-
- titre
- Meta-Programming for Proof Transfer in Dependent Type Theory
- auteur
- Enzo Crance
- article
- Informatique. Nantes Université, 2023. Français. ⟨NNT : 2023NANU4071⟩
- typdoc
- Theses
- Accès au texte intégral et bibtex
-
- 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
-
Preprints, Working Papers, ...
- 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
-
- titre
- Pursuing Shtuck
- auteur
- Pierre-Marie Pédrot
- article
- 2023
- typdoc
- Preprints, Working Papers, ...
- Accès au texte intégral et 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
-
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, ⟨10.1145/3547655⟩
- typdoc
- Journal articles
- Accès au texte intégral et 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
-
- 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
-
- 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
-
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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
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
-
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
-
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
-
- titre
- Typage Bidirectionnel pour le Calcul des Constructions Inductives
- 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
-
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
-
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
-
- 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
-
- 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
-
- 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
-
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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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 texte intégral et 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
-
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
-
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
-
- 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
-
- 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
-
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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
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
-
- 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
-
- 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, ⟨10.1007/978-3-030-51054-1_1⟩
- typdoc
- Conference papers
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- 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
-
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
-
- 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
-
- 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
-
- 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
-
- 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/3290316⟩
- typdoc
- Journal articles
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
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
-
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
-
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
-
- 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
-
- titre
- An implementation of polygraphs
- auteur
- Maxime Lucas
- article
- 2019
- typdoc
- Preprints, Working Papers, ...
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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, ⟨10.1145/3209108.3209133⟩
- typdoc
- Conference papers
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- 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
-
- 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
-
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
-
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
-
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
-
- 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
-
Software
- titre
- The Coq Proof Assistant, version 8.8.0
- auteur
- The Coq Development Team
- article
- 2018
- typdoc
- Software
- Accès au 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
-
- 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
-
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
-
- titre
- Resource Polymorphism
- auteur
- Guillaume Munch-Maccagnoni
- article
- 2018
- typdoc
- Preprints, Working Papers, ...
- Accès au texte intégral et bibtex
-
2017
Journal articles
- 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
-
- 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
-
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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
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
-
- 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
-