Sites Inria

English version

Equipe de recherche GALLINETTE

Publications de l'équipe GALLINETTE

2019

Communication dans un congrès

titre
Eliminating Reflection from Type Theory
auteur
Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau
article
CPP 2019 - The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Lisbonne, Portugal. pp.1-19, 2019, . <10.1145/nnnnnnn.nnnnnnn>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01849166/file/cpp19.pdf BibTex
titre
Definitional Proof-Irrelevance without K
auteur
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau
article
46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019, Jan 2019, Lisbon, Portugal. 2019, POPL
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01859964/file/main_popl.pdf BibTex

2018

Article dans une revue

titre
Goodwillie's calculus of functors and higher topos theory
auteur
Mathieu Anel, Georg Biedermann, Eric Finster, André Joyal
article
Journal of topology, Oxford University Press, 2018, 11 (4), pp.1100-1132. <10.1112/topo.12082>
Accès au bibtex
BibTex
titre
Preface: Special Issue on Homotopy Type Theory and Univalent Foundations
auteur
Peter Lefanu Lumsdaine, Nicolas Tabareau
article
Journal of Automated Reasoning, Springer Verlag, 2018, <10.1007/s10817-018-9491-3>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01929871/file/main.pdf BibTex
titre
Chemical foundations of distributed aspects
auteur
Nicolas Tabareau, Eric Tanter
article
Distributed Computing, Springer Verlag, 2018, pp.1-24. <10.1007/s00446-018-0334-6>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01811884/file/main.pdf BibTex
titre
Formally Verified Approximations of Definite Integrals
auteur
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
article
Journal of Automated Reasoning, Springer Verlag, 2018, pp.1-20. <10.1007/s10817-018-9463-7>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01630143/file/main.pdf BibTex
titre
Foundations of Dependent Interoperability
auteur
Pierre-Evariste Dagand, Nicolas Tabareau, Éric Tanter
article
Journal of Functional Programming, Cambridge University Press (CUP), 2018, 28, <10.1017/S0956796818000011>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01629909/file/main.pdf BibTex

Communication dans un congrès

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
ICFP 2018 - International Conference on Functional Programming, Sep 2018, St. Louis, United States. ACM, 2 (ICFP), pp.1-30, 2018, <10.1145/3236792>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01883524/file/ICFP18-modules.pdf BibTex
titre
Equivalences for Free
auteur
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
article
ICFP 2018 - International Conference on Functional Programming, Sep 2018, Saint-Louis, United States. pp.1-29, 2018, <10.1145/3234615>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01559073/file/main_icfp.pdf 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. ACM Press, pp.1-13, 2018, <10.1145/3236950.3236955>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01883559/file/PPDP18-cert-comp-fin.pdf BibTex
titre
A sequent calculus with dependent types for classical arithmetic
auteur
Étienne Miquey
article
LICS 2018 - 33th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford, United Kingdom. ACM, pp.720-729, <10.1145/3209108.3209199>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01703526/file/dlpaw.pdf BibTex
titre
Formalizing Implicative Algebras in Coq
auteur
Étienne Miquey
article
ITP 2018 - 9th International Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. Springer, 10895, pp.459-476, LNCS. <10.1007/978-3-319-94821-8_27>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01703524/file/impalg.pdf BibTex
titre
Every $λ$-Term is Meaningful for the Infinitary Relational Model
auteur
Pierre Vial
article
LICS 2018 - Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford, United Kingdom. pp.1-26, <10.1145/nnnnnnn.nnnnnnn>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01840744/file/hal-inf-rel-mod-conf.pdf BibTex
titre
Towards Certified Meta-Programming with Typed Template-Coq
auteur
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau
article
ITP 2018 - 9th Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. Springer, 10895, pp.20-39, 2018, LNCS. <10.1007/978-3-319-94821-8_2>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01809681/file/paper_39.pdf BibTex
titre
A resource modality for RAII
auteur
Guillaume Combette, Guillaume Munch-Maccagnoni
article
LOLA 2018: Workshop on Syntax and Semantics of Low-Level Languages, Jul 2018, Oxford, United Kingdom. pp.1-4
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01806634/file/raii-modality-short.pdf BibTex
titre
Realizability Interpretation and Normalization of Typed Call-by-Need $λ$-calculus With Control
auteur
Étienne Miquey, Hugo Herbelin
article
Christel Baier; Ugo Dal Lago. FOSSACS 18 - 21st International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessalonique, Greece. Springer, 10803, pp.276-292, LNCS. <10.1007/978-3-319-89366-2_15>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01624839/file/cbncps.pdf BibTex
titre
Failure is Not an Option An Exceptional Type Theory
auteur
Pierre-Marie Pédrot, Nicolas Tabareau
article
ESOP 2018 - 27th European Symposium on Programming, Apr 2018, Thessaloniki, Greece. Springer, 10801, pp.245-271, LNCS. <10.1007/978-3-319-89884-1_9>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01840643/file/main.pdf BibTex
titre
Typed Template Coq -- Certified Meta-Programming in Coq
auteur
Abhishek Anand, Simon Boulier, Nicolas Tabareau, Matthieu Sozeau
article
CoqPL 2018 - The Fourth International Workshop on Coq for Programming Languages, Jan 2018, Los Angeles, CA, United States. pp.1-2
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01671948/file/Anand-Boulier-Tabareau-Sozeau-CoqPL18.pdf BibTex

Autre publication

titre
High-level signatures and initial semantics
auteur
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
article
2018, pp.1-20. <10.4230/LIPIcs.CSL.2018.4>
Accès au bibtex
https://arxiv.org/pdf/1805.03740 BibTex

Rapport

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
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01374721/file/1609.08925v2.pdf BibTex
titre
The Abstract Accountability Language: its Syntax, Semantics and Tools
auteur
Walid Benghabrit, Hervé Grall, Jean-Claude Royer, Anderson Santana de Oliveira
article
[Research Report] IMT Atlantique. 2018
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01856329/file/main.pdf BibTex

Pré-publication, Document de travail

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

2017

Article dans une revue

titre
Normalization by evaluation for sized dependent types
auteur
Andreas Abel, Andrea Vezzosi, Théo Winterhalter
article
Proceedings of the ACM on Programming Languages, ACM, 2017, 1, pp.33. <10.1145/3110277>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01596179/file/icfp17-main84.pdf BibTex

Communication dans un congrès

titre
Displayed Categories
auteur
Benedikt Ahrens, Peter Lumsdaine
article
Dale Miller. 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Sep 2017, Oxford, United Kingdom. Leibniz International Proceedings in Informatics (LIPIcs), 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), 84 (5:1--5:16), 2017, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). <10.4230/LIPIcs.FSCD.2017.5>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01584770/file/LIPIcs-FSCD-2017-5.pdf BibTex
titre
Categorical Structures for Type Theory in Univalent Foundations
auteur
Benedikt Ahrens, Peter Lefanu Lumsdaine, Vladimir Voevodsky
article
Valentin Goranko and Mads Dam. 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Aug 2017, Stockholm, Sweden. LIPIcs, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), 82, pp.8:1 - 8:16, 2017, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). <10.4230/LIPIcs.CSL.2017.8>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01579271/file/LIPIcs-CSL-2017-8.pdf BibTex
titre
An Effectful Way to Eliminate Addiction to Dependence
auteur
Pierre-Marie Pédrot, Nicolas Tabareau
article
Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on, Jun 2017, Reykjavik, Iceland. pp.12, 2017, <10.1109/LICS.2017.8005113>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01441829/file/main.pdf BibTex
titre
The next 700 syntactical models of type theory
auteur
Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau
article
Certified Programs and Proofs (CPP 2017), Jan 2017, Paris, France. pp.182 - 194, 2017, <10.1145/3018610.3018620>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01445835/file/main.pdf BibTex

Pré-publication, Document de travail

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

Suivez Inria