Enrico Tassi

ORCID

Publication Activity (10 Years)

Years Active: 2001-2023
Publications (10 Years): 11

Top Venues

ITP

CoRR

MKM/Calculemus/DML

Math. Struct. Comput. Sci.

University of Bologna, Italy (PHD)

Education History

University of Bologna, Italy

PHD

Publications

Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. CPP (2023)
Karl Palmskog, Enrico Tassi, Théo Zimmermann
Reliably Reproducing Machine-Checked Proofs with the Coq Platform. CoRR (2022)
Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi
Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description). FSCD (2020)
Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
Implementing type theory in higher order constraint logic programming. Math. Struct. Comput. Sci. 29 (8) (2019)
Enrico Tassi
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. ITP (2019)
Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
Coqoon - An IDE for interactive proof development in Coq. Int. J. Softw. Tools Technol. Transf. 20 (2) (2018)
Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
Coqoon - An IDE for Interactive Proof Development in Coq. TACAS (2016)
Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi
Implementing HOL in an Higher Order Logic Programming Language. LFMTP (2016)
Bruno Barras, Carst Tankink, Enrico Tassi
Asynchronous processing of Coq documents: from the kernel up to the user interface. CoRR (2015)
Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
ELPI: Fast, Embeddable, \lambda Prolog Interpreter. LPAR (2015)
Bruno Barras, Carst Tankink, Enrico Tassi
Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface. ITP (2015)
Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). ITP (2014)
Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. MKM/Calculemus/DML (2013)
Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. CoRR (2013)
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
A Machine-Checked Proof of the Odd Order Theorem. ITP (2013)
Assia Mahboubi, Enrico Tassi
Canonical Structures for the Working Coq User. ITP (2013)
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover. J. Autom. Reason. 49 (3) (2012)
Georges Gonthier, Enrico Tassi
A Language of Patterns for Subterm Selection. ITP (2012)
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions Log. Methods Comput. Sci. 8 (1) (2012)
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
The Matita Interactive Theorem Prover. CADE (2011)
Claudio Sacerdoti Coen, Enrico Tassi
Formalising Overlap Algebras in Matita. Math. Struct. Comput. Sci. 21 (4) (2011)
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi
Regular Expressions, au point CoRR (2010)
Andrea Asperti, Enrico Tassi
Smart Matching. AISC/MKM/Calculemus (2010)
Andrea Asperti, Enrico Tassi
Smart matching CoRR (2010)
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
Hints in Unification. TPHOLs (2009)
Andrea Asperti, Enrico Tassi
An Interactive Driver for Goal-directed Proof Strategies. Electron. Notes Theor. Comput. Sci. 226 (2009)
Claudio Sacerdoti Coen, Enrico Tassi
Natural Deduction Environment for Matita. Calculemus/MKM (2009)
Andrea Asperti, Enrico Tassi
Superposition as a logical glue TYPES (2009)
Claudio Sacerdoti Coen, Enrico Tassi
Nonuniform Coercions via Unification Hints TYPES (2009)
Claudio Sacerdoti Coen, Enrico Tassi
A constructive and formal proof of Lebesgue's Dominated Convergence Theorem in the interactive theorem prover Matita. J. Formaliz. Reason. 1 (1) (2008)
Andrea Asperti, Enrico Tassi
Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case. Calculemus/MKM (2007)
Claudio Sacerdoti Coen, Enrico Tassi
Working with Mathematical Structures in Type Theory. TYPES (2007)
Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
Tinycals: Step by Step Tacticals. Electron. Notes Theor. Comput. Sci. 174 (2) (2007)
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
A Modular Formalisation of Finite Group Theory. TPHOLs (2007)
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
User Interaction with the Matita Proof Assistant. J. Autom. Reason. 39 (2) (2007)
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
Crafting a Proof Assistant. TYPES (2006)
Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
A Content Based Mathematical Search Engine: Whelp. TYPES (2004)
L. A. T. Bauerdick, Adrian Fox-Murphy, Tobias Haas, Stefan Stonjek, Enrico Tassi
Event Indexing Systems for Efficient Selection and Analysis of HERA Data CoRR (2001)

Enrico Tassi.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Enrico Tassi