Publications HAL de Simon,Boulier;Théo,Winterhalter;Xavier,Montillet;Ambroise,Lafont;Gaëtan,Gilbert;Igor,Zhirkov;Eric,Finster;Pierre,Vial;Etienne,Miquey;Julien,Cohen;Guillaume,Munch-Maccagnoni;Hervé,Graal;Rémi,Douence;Assia,Mahboubi;Nicolas,Tabareau;Kevin,Quirin;Pierre-Marie,Pédrot;Benedikt,Ahrens de la structure Gallinette

2018

Conference papers

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
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01671948/file/Anand-Boulier-Tabareau-Sozeau-CoqPL18.pdf BibTex

2017

Journal articles

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〉
typdoc
Journal articles
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01596179/file/icfp17-main84.pdf BibTex

Conference papers

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〉
typdoc
Conference papers
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〉
typdoc
Conference papers
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〉
typdoc
Conference papers
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〉
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01445835/file/main.pdf BibTex

Preprints, Working Papers, ...

titre
Foundations of Dependent Interoperability
auteur
Pierre-Evariste Dagand, Nicolas Tabareau, Éric Tanter
article
2017
typdoc
Preprints, Working Papers, ...
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
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01559073/file/main.pdf BibTex
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
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
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01528857/file/curry.pdf BibTex