Publications HAL

2022

titre
Practical and sound equality tests, automatically Deriving eqType instances for Jasmin's data types with Coq-Elpi
auteur
Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi
article
2022
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03800154/file/feqb.pdf BibTex
titre
Reliably Reproducing Machine-Checked Proofs with the Coq Platform
auteur
Karl Palmskog, Enrico Tassi, Théo Zimmermann
article
RRRR 2022 - Workshop on Reproducibility and Replication of Research Results, Apr 2022, Munich, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03592675/file/main.pdf BibTex

2021

titre
Porting the Mathematical Components library to Hierarchy Builder
auteur
Reynald Affeldt, Xavier Allamigeon, Yves Bertot, Quentin Canu, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Théry, Anton Trunov
article
the COQ Workshop 2021, Jul 2021, virtuel- Rome, Italy
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-03463762/file/DTIS21240.pdf BibTex

2020

titre
Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi
auteur
Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi
article
FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. pp.34:1--34:21, ⟨10.4230/LIPIcs.FSCD.2020.34⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02478907/file/LIPIcs-FSCD-2020-34.pdf BibTex
titre
Private types in Higher Order Logic Programming
auteur
Marco Maggesi, Enrico Tassi
article
TEASE-LP 2020 - Workshop on Trends, Extensions, Applications and Semantics of Logic Programming, May 2020, Virtual Event, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03117762/file/privtypes.pdf BibTex

2019

titre
Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq
auteur
Enrico Tassi
article
ITP 2019 - 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨10.4230/LIPIcs.CVIT.2016.23⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01897468/file/induction.pdf BibTex
titre
Implementing Type Theory in Higher Order Constraint Logic Programming
auteur
Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2019, 29 (8), pp.1125-1150
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01410567/file/dalefest.pdf BibTex

2018

titre
Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect)
auteur
Enrico Tassi
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01637063/file/coqpl2018.pdf BibTex

2017

titre
Coqoon
auteur
Alexander Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
article
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01410450/file/main-sttt.pdf BibTex

2016

titre
A Small Scale Reflection Extension for the Coq system
auteur
Georges Gonthier, Assia Mahboubi, Enrico Tassi
article
[Research Report] RR-6455, Inria Saclay Ile de France. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00258384/file/main.pdf BibTex
titre
Boolean reflection via type classes
auteur
Benjamin Grégoire, Enrico Tassi
article
Coq Workshop, Aug 2016, Nancy, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01410530/file/autoview.pdf BibTex
titre
Coqoon An IDE for interactive proof development in Coq
auteur
Alexander Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
article
TACAS, Apr 2016, Eindhoven, Netherlands
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01242295/file/main.pdf BibTex
titre
Implementing HOL in an Higher Order Logic Programming Language
auteur
Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi
article
Logical Frameworks and Meta Languages: Theory and Practice, Jun 2016, Porto, Portugal. pp.10, ⟨10.1145/2966268.2966272⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01394686/file/holsuperlight.pdf BibTex

2015

titre
Asynchronous processing of Coq documents: from the kernel up to the user interface
auteur
Bruno Barras, Carst Tankink, Enrico Tassi
article
Proceedings of ITP, Aug 2015, Nanjing, China
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01135919/file/full.pdf BibTex
titre
ELPI: fast, Embeddable, λProlog Interpreter
auteur
Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
article
Proceedings of LPAR, Nov 2015, Suva, Fiji
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01176856/file/lpar2015.pdf BibTex

2014

titre
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
auteur
Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi
article
ITP - 5th International Conference on Interactive Theorem Proving, 2014, Vienna, Austria
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00984057/file/main.pdf BibTex
titre
Coq 8.4 Reference Manual
auteur
Pierre Boutillier, Stephane Glondu, Benjamin Grégoire, Hugo Herbelin, Pierre Letouzey, Pierre-Marie Pédrot, Yann Régis-Gianas, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi
article
[Research Report] Inria. 2014
Accès au bibtex
BibTex

2013

titre
A Machine-Checked Proof of the Odd Order Theorem
auteur
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
article
ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00816699/file/main.pdf BibTex
titre
Canonical Structures for the working Coq user
auteur
Assia Mahboubi, Enrico Tassi
article
ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.19-34, ⟨10.1007/978-3-642-39634-2_5⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00816703/file/main.pdf BibTex
titre
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
auteur
Bruno Barras, Lourdes del Carmen Gonzalez Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
article
MKM/Calculemus/DML, Jul 2013, Bath, United Kingdom. pp.359-363
Accès au bibtex
BibTex

2012

titre
A language of patterns for subterm selection
auteur
Georges Gonthier, Enrico Tassi
article
ITP, Aug 2012, Princeton, United States. pp.361-376, ⟨10.1007/978-3-642-32347-8_25⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00652286/file/rew.pdf BibTex

2007

titre
A Modular Formalisation of Finite Group Theory
auteur
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
article
[Research Report] RR-6156, INRIA. 2007, pp.17
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00139131/file/RR-6156.pdf BibTex