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

Journal articles

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

Conference papers

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〉
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01559073/file/main_icfp.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. pp.1-18, 2018
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01809681/file/paper_39.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. pp.1-22
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01703526/file/dlpaw.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〉
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01840744/file/hal-inf-rel-mod-conf.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
typdoc
Conference papers
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
FOSSACS 18 - 21st International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessalonique, Greece. pp.1-23
typdoc
Conference papers
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. pp.1-32
typdoc
Conference papers
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
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
titre
Formalizing Implicative Algebras in Coq
auteur
Étienne Miquey
article
Interactive Theorem Proving, 2018, Oxford, United Kingdom. 〈10.1007/978-3-319-94821-8_27〉
typdoc
Conference papers
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01703524/file/impalg.pdf BibTex

Preprints, Working Papers, ...

titre
Definitional Proof-Irrelevance without K
auteur
Gaëtan Gilbert, Cockx Jesper, Sozeau Matthieu, Nicolas Tabareau
article
2018
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01859964/file/main_popl.pdf BibTex
titre
Eliminating Reflection from Type Theory: To the Legacy of Martin Hofmann
auteur
Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau
article
2018
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01849166/file/ett-to-itt-hal.pdf BibTex
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
https://hal.archives-ouvertes.fr/hal-01744359/file/dL-extended.pdf BibTex
titre
Resource Polymorphism
auteur
Guillaume Munch-Maccagnoni
article
2018
typdoc
Preprints, Working Papers, ...
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01724997/file/ocaml-raii.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
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