Mathematical knowledge management in HELM A Asperti, L Padovani, C Sacerdoti Coen, F Guidi, I Schena Annals of Mathematics and Artificial Intelligence 38 (1), 27-46, 2003 | 95 | 2003 |

A content based mathematical search engine: Whelp A Asperti, F Guidi, C Sacerdoti Coen, E Tassi, S Zacchiroli Types for Proofs and Programs, 17-32, 2006 | 74 | 2006 |

A survey on retrieval of mathematical knowledge F Guidi, C Sacerdoti Coen Mathematics in Computer Science 10 (4), 409-427, 2016 | 56 | 2016 |

ELPI: Fast, Embeddable, Prolog Interpreter C Dunchev, F Guidi, C Sacerdoti Coen, E Tassi Logic for Programming, Artificial Intelligence, and Reasoning, 460-468, 2015 | 47 | 2015 |

A query language for a metadata framework about mathematical resources F Guidi, I Schena International Conference on Mathematical Knowledge Management, 105-118, 2003 | 38 | 2003 |

Searching and Retrieving in Content-based Repositories of Formal Mathematical Knowledge F Guidi PhD thesis. UBLCS 2003-06, Università di Bologna, 2003 | 21 | 2003 |

The formal system λδ F Guidi ACM Transactions on Computational Logic (TOCL) 11 (1), Article n. 5, 2009 | 18 | 2009 |

Querying distributed digital libraries of mathematics F Guidi, C Sacerdoti Coen 11th Symposium on the Integration of Symbolic Computation and Mechanized …, 2003 | 18 | 2003 |

Implementing type theory in higher order constraint logic programming F Guidi, CS Coen, E Tassi Mathematical Structures in Computer Science 29 (8), 1125-1150, 2019 | 10 | 2019 |

Procedural representation of cic proof terms F Guidi Journal of Automated Reasoning 44 (1), 53-78, 2010 | 8 | 2010 |

Verified Representations of Landau's" Grundlagen" in the lambda-delta Family and in the Calculus of Constructions F Guidi Journal of Formalized Reasoning 8 (1), 93-116, 2015 | 5 | 2015 |

Landau’s “Grundlagen der Analysis” from Automath to lambda-delta F Guidi Tec. Rep. UBLCS 2009-16, Università di Bologna, 2009 | 4 | 2009 |

λ-Types on the λ-Calculus with Abbreviations F Guidi arXiv preprint cs/0611040, 2006 | 4 | 2006 |

Extending the Applicability Condition in the Formal System F Guidi arXiv preprint arXiv:1411.0154, 2014 | 3 | 2014 |

Standardization and confluence in pure lambda-calculus formalized for the matita theorem prover F Guidi Journal of Formalized Reasoning 5 (1), 1-25, 2012 | 3 | 2012 |

An Efficient Validation Procedure for the Formal System λδ F Guidi 6th Conference on Computability in Europe (CiE 2010), CMATI Booklet, 204-213, 2010 | 2* | 2010 |

λ-Types on the λ-Calculus with Abbreviations: a Certified Specification F Guidi Tech. Rep. UBLCS 2006-01, Università di Bologna, 2006 | 2 | 2006 |

The Formal System λδ Revised - Stage A: Extending the Applicability Condition F Guidi arXiv preprint arXiv:1411.0154, 2014 | 1 | 2014 |

A formal system for the universal quantification of schematic variables F Guidi ACM Transactions on Computational Logic (TOCL) 23 (1), 1-37, 2021 | | 2021 |

Two Formal Systems of the λδ Family Revised F Guidi arXiv preprint arXiv:1911.12749, 2019 | | 2019 |