Event Indexing Systems for Efficient Selection and Analysis of HERA Data - L. A. T. Bauerdick; Adrian Fox-Murphy; Tobias Haas; Stefan Stonjek; Enrico Tassi (CoRR, 2001)

A Content Based Mathematical Search Engine: Whelp. - Andrea Asperti; Ferruccio Guidi; Claudio Sacerdoti Coen; Enrico Tassi; Stefano Zacchiroli (TYPES, 2004)

Crafting a Proof Assistant. - Andrea Asperti; Claudio Sacerdoti Coen; Enrico Tassi; Stefano Zacchiroli (TYPES, 2006)

Tinycals: Step by Step Tacticals. - Claudio Sacerdoti Coen; Enrico Tassi; Stefano Zacchiroli (UITP@FLoC, 2006)

Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case. - Andrea Asperti; Enrico Tassi (Calculemus/MKM, 2007)

A Modular Formalisation of Finite Group Theory. - Georges Gonthier; Assia Mahboubi; Laurence Rideau; Enrico Tassi; Laurent Théry (TPHOLs, 2007)

Working with Mathematical Structures in Type Theory. - Claudio Sacerdoti Coen; Enrico Tassi (TYPES, 2007)

User Interaction with the Matita Proof Assistant. - Andrea Asperti; Claudio Sacerdoti Coen; Enrico Tassi; Stefano Zacchiroli (J. Autom. Reason., 2007)

An Interactive Driver for Goal-directed Proof Strategies. - Andrea Asperti; Enrico Tassi (UITP@TPHOLs, 2008)

A constructive and formal proof of Lebesgue's Dominated Convergence Theorem in the interactive theorem prover Matita. - Claudio Sacerdoti Coen; Enrico Tassi (J. Formaliz. Reason., 2008)

Interactive theorem provers: issues faced as a user and tackled as a developer. - Enrico Tassi (2008)

Natural Deduction Environment for Matita. - Claudio Sacerdoti Coen; Enrico Tassi (Calculemus/MKM, 2009)

Hints in Unification. - Andrea Asperti; Wilmer Ricciotti; Claudio Sacerdoti Coen; Enrico Tassi (TPHOLs, 2009)

Superposition as a logical glue - Andrea Asperti; Enrico Tassi (TYPES, 2009)

Nonuniform Coercions via Unification Hints - Claudio Sacerdoti Coen; Enrico Tassi (TYPES, 2009)

Smart Matching. - Andrea Asperti; Enrico Tassi (AISC/MKM/Calculemus, 2010)

Regular Expressions, au point - Andrea Asperti; Claudio Sacerdoti Coen; Enrico Tassi (CoRR, 2010)

The Matita Interactive Theorem Prover. - Andrea Asperti; Wilmer Ricciotti; Claudio Sacerdoti Coen; Enrico Tassi (CADE, 2011)

Formalising Overlap Algebras in Matita. - Claudio Sacerdoti Coen; Enrico Tassi (Math. Struct. Comput. Sci., 2011)

A Language of Patterns for Subterm Selection. - Georges Gonthier; Enrico Tassi (ITP, 2012)

A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions - Andrea Asperti; Wilmer Ricciotti; Claudio Sacerdoti Coen; Enrico Tassi (Log. Methods Comput. Sci., 2012)

Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover. - Andrea Asperti; Wilmer Ricciotti; Claudio Sacerdoti Coen; Enrico Tassi (J. Autom. Reason., 2012)

A Machine-Checked Proof of the Odd Order Theorem. - Georges Gonthier; Andrea Asperti; Jeremy Avigad; Yves Bertot; Cyril Cohen; François Garillot; Stéphane Le Roux 001; Assia Mahboubi; Russell O'Connor; Sidi Ould Biha; Ioana Pasca; Laurence Rideau; et al. (ITP, 2013)

Canonical Structures for the Working Coq User. - Assia Mahboubi; Enrico Tassi (ITP, 2013)

Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. - Bruno Barras; Lourdes Del Carmen González-Huesca; Hugo Herbelin; Yann Régis-Gianas; Enrico Tassi; Makarius Wenzel; Burkhart Wolff (MKM/Calculemus/DML, 2013)

A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). - Frédéric Chyzak; Assia Mahboubi; Thomas Sibut-Pinote; Enrico Tassi (ITP, 2014)

Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface. - Bruno Barras; Carst Tankink; Enrico Tassi (ITP, 2015)

ELPI: Fast, Embeddable, λProlog Interpreter. - Cvetan Dunchev; Ferruccio Guidi; Claudio Sacerdoti Coen; Enrico Tassi (LPAR, 2015)

Implementing HOL in an Higher Order Logic Programming Language. - Cvetan Dunchev; Claudio Sacerdoti Coen; Enrico Tassi (LFMTP, 2016)

Coqoon - An IDE for interactive proof development in Coq. - Alexander John Faithfull; Jesper Bengtson; Enrico Tassi; Carst Tankink (Int. J. Softw. Tools Technol. Transf., 2018)

Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. - Enrico Tassi (ITP, 2019)

Implementing type theory in higher order constraint logic programming. - Ferruccio Guidi; Claudio Sacerdoti Coen; Enrico Tassi (Math. Struct. Comput. Sci., 2019)

Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description). - Cyril Cohen; Kazuhiko Sakaguchi; Enrico Tassi (FSCD, 2020)

Reliably Reproducing Machine-Checked Proofs with the Coq Platform. - Karl Palmskog; Enrico Tassi; Théo Zimmermann (CoRR, 2022)

Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. - Benjamin Grégoire; Jean-Christophe Léchenet; Enrico Tassi (CPP, 2023)

Higher-Order unification for free!: Reusing the meta-language unification for the object language. - Davide Fissore; Enrico Tassi (PPDP, 2024)