Sites Inria

English version

Equipe de recherche GALLINETTE

Publications de l'équipe GALLINETTE

2018

Article dans une revue

titre
Formally Verified Approximations of Definite Integrals
auteur
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
article
Journal of Automated Reasoning, Springer Verlag, 2018, 〈10.1007/s10817-018-9463-7〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01630143/file/main.pdf BibTex

Communication dans un congrès

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
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01624839/file/cbncps.pdf BibTex
titre
Typed Template Coq -- Certified Meta-Programming in Coq
auteur
Abhishek Anand, Simon Boulier, Nicolas Tabareau, Matthieu Sozeau
article
The Fourth International Workshop on Coq for Programming Languages, Jan 2018, Los Angeles, CA, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01671948/file/Anand-Boulier-Tabareau-Sozeau-CoqPL18.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
titre
A sequent calculus with dependent types for classical arithmetic
auteur
Étienne Miquey
article
2018
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
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01703524/file/impalg.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
Foundations of Dependent Interoperability
auteur
Pierre-Evariste Dagand, Nicolas Tabareau, Éric Tanter
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01629909/file/main.pdf BibTex
titre
Equivalences for Free!
auteur
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01559073/file/main_icfp.pdf BibTex
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 tout au long de son 50e anniversaire et au-delà !