Enrico Tassi

43 papers A 2B 10C 2Journal 13Unranked 14
YearRankTypeTitle / Venue / Authors
2026 C conf
Determinacy Checking for Elpi: an Higher-Order Logic Programming Language with Cut.
PADL
Davide Fissore, Enrico Tassi
2025 B conf
Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic.
ITP
Robbert Krebbers, Luko van der Maas, Enrico Tassi
2024 C conf
Higher-Order unification for free!: Reusing the meta-language unification for the object language.
PPDP
Davide Fissore, Enrico Tassi
2023 B conf
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi.
CPP
Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi
2022 J jnl
Reliably Reproducing Machine-Checked Proofs with the Coq Platform.
CoRR
Karl Palmskog, Enrico Tassi, Théo Zimmermann
2021 — ed.
Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021.
LFMTP
Elaine Pimentel, Enrico Tassi
2020 B conf
Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description).
FSCD
Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi
2019 B conf
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq.
ITP
Enrico Tassi
2019 J jnl
Implementing type theory in higher order constraint logic programming.
Math. Struct. Comput. Sci.
Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
2018 J jnl
Coqoon - An IDE for interactive proof development in Coq.
Int. J. Softw. Tools Technol. Transf.
Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
2016 A conf
Coqoon - An IDE for Interactive Proof Development in Coq.
TACAS
Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
2016 — conf
Implementing HOL in an Higher Order Logic Programming Language.
LFMTP
Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi
2015 B conf
Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface.
ITP
Bruno Barras, Carst Tankink, Enrico Tassi
2015 J jnl
Asynchronous processing of Coq documents: from the kernel up to the user interface.
CoRR
Bruno Barras, Carst Tankink, Enrico Tassi
2015 B conf
ELPI: Fast, Embeddable, λProlog Interpreter.
LPAR
Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
2014 B conf
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3).
ITP
Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi
2013 B conf
A Machine-Checked Proof of the Odd Order Theorem.
ITP
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
2013 B conf
Canonical Structures for the Working Coq User.
ITP
Assia Mahboubi, Enrico Tassi
2013 — conf
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems.
MKM/Calculemus/DML
Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
2013 J jnl
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems.
CoRR
Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
2012 J jnl
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
Log. Methods Comput. Sci.
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
2012 B conf
A Language of Patterns for Subterm Selection.
ITP
Georges Gonthier, Enrico Tassi
2012 J jnl
Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover.
J. Autom. Reason.
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
2011 J jnl
Formalising Overlap Algebras in Matita.
Math. Struct. Comput. Sci.
Claudio Sacerdoti Coen, Enrico Tassi
2011 A conf
The Matita Interactive Theorem Prover.
CADE
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
2010 J jnl
Regular Expressions, au point
CoRR
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi
2010 — conf
Smart Matching.
AISC/MKM/Calculemus
Andrea Asperti, Enrico Tassi
2010 J jnl
Smart matching
CoRR
Andrea Asperti, Enrico Tassi
2009 — conf
Hints in Unification.
TPHOLs
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
2009 — conf
Natural Deduction Environment for Matita.
Calculemus/MKM
Claudio Sacerdoti Coen, Enrico Tassi
2009 — conf
Nonuniform Coercions via Unification Hints
TYPES
Claudio Sacerdoti Coen, Enrico Tassi
2009 — conf
Superposition as a logical glue
TYPES
Andrea Asperti, Enrico Tassi
2008 J jnl
A constructive and formal proof of Lebesgue's Dominated Convergence Theorem in the interactive theorem prover Matita.
J. Formaliz. Reason.
Claudio Sacerdoti Coen, Enrico Tassi
2008 — conf
An Interactive Driver for Goal-directed Proof Strategies.
UITP@TPHOLs
Andrea Asperti, Enrico Tassi
2008 — —
Interactive theorem provers: issues faced as a user and tackled as a developer.
Enrico Tassi
2007 — conf
A Modular Formalisation of Finite Group Theory.
TPHOLs
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
2007 — conf
Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case.
Calculemus/MKM
Andrea Asperti, Enrico Tassi
2007 J jnl
User Interaction with the Matita Proof Assistant.
J. Autom. Reason.
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
2007 — conf
Working with Mathematical Structures in Type Theory.
TYPES
Claudio Sacerdoti Coen, Enrico Tassi
2006 — conf
Crafting a Proof Assistant.
TYPES
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
2006 — conf
Tinycals: Step by Step Tacticals.
UITP@FLoC
Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
2004 — conf
A Content Based Mathematical Search Engine: Whelp.
TYPES
Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
2001 J jnl
Event Indexing Systems for Efficient Selection and Analysis of HERA Data
CoRR
L. A. T. Bauerdick, Adrian Fox-Murphy, Tobias Haas, Stefan Stonjek, Enrico Tassi