Publications HAL

2024

titre: Higher-Order unification for free!
auteur: Davide Fissore, Enrico Tassi
article: PPDP 2024: 26th International Symposium on Principles and Practice of Declarative Programming, ACM, pp.1-13, 2024, ⟨10.1145/3678232.3678233⟩
Accès au texte intégral et bibtex

2023

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: CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2023, Boston MA USA, France. pp.167-181, ⟨10.1145/3573105.3575683⟩
Accès au texte intégral et bibtex

2022

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

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

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

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

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

titre: Implementing Type Theory in Higher Order Constraint Logic Programming
auteur: Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
article: Mathematical Structures in Computer Science, 2019, 29 (8), pp.1125-1150
Accès au texte intégral et bibtex

2018

titre: Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect)
auteur: Enrico Tassi
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

2017

titre: Coqoon
auteur: Alexander Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
article: International Journal on Software Tools for Technology Transfer, 2017
Accès au texte intégral et bibtex

2016

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

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

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

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

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

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

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

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

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

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