A Query Language for a Metadata Framework about Mathematical Resources. - Ferruccio Guidi; Irene Schena (MKM, 2003)

Mathematical Knowledge Management in HELM. - Andrea Asperti; Luca Padovani; Claudio Sacerdoti Coen; Ferruccio Guidi; Irene Schena (Ann. Math. Artif. Intell., 2003)

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

Lambda Types on the Lambda Calculus with Abbreviations - Ferruccio Guidi (CoRR, 2006)

The formal system lambdadelta. - Ferruccio Guidi (ACM Trans. Comput. Log., 2009)

Procedural Representation of CIC Proof Terms. - Ferruccio Guidi (J. Autom. Reason., 2010)

Type systems for dummies. - Andrea Asperti; Ferruccio Guidi (TLDI, 2012)

Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover. - Ferruccio Guidi (J. Formaliz. Reason., 2012)

The Formal System λδ Revised - Stage A: Extending the Applicability Condition. - Ferruccio Guidi (CoRR, 2014)

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

Verified Representations of Landau's "Grundlagen" in the lambda-delta Family and in the Calculus of Constructions. - Ferruccio Guidi (J. Formaliz. Reason., 2015)

A Survey on Retrieval of Mathematical Knowledge. - Ferruccio Guidi; Claudio Sacerdoti Coen (Math. Comput. Sci., 2016)

Two Formal Systems of the $λδ$ Family Revised. - Ferruccio Guidi (CoRR, 2019)

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

A Formal System for the Universal Quantification of Schematic Variables. - Ferruccio Guidi (ACM Trans. Comput. Log., 2022)