Mathematical knowledge management in HELM A Asperti, L Padovani, C Sacerdoti Coen, F Guidi, I Schena
Annals of Mathematics and Artificial Intelligence 38, 27-46, 2003
102 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
78 2006 ELPI: fast, embeddable, prolog interpreter C Dunchev, F Guidi, C Sacerdoti Coen, E Tassi
Logic for Programming, Artificial Intelligence, and Reasoning, 460-468, 2015
66 2015 A survey on retrieval of mathematical knowledge F Guidi, C Sacerdoti Coen
Mathematics in Computer Science 10 (4), 409-427, 2016
53 2016 A query language for a metadata framework about mathematical resources F Guidi, I Schena
Mathematical Knowledge Management: Second International Conference, MKM 2003 …, 2003
40 2003 A survey on retrieval of mathematical knowledge F Guidi, C Sacerdoti Coen
International Conference on Intelligent Computer Mathematics, 296-315, 2015
31 2015 Searching and Retrieving in Content-based Repositories of Formal Mathematical Knowledge F Guidi
PhD thesis. UBLCS 2003-06, Università di Bologna, 2003
21 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
18 2019 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 Procedural representation of cic proof terms F Guidi
Journal of Automated Reasoning 44, 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
6 2015 Standardization and confluence in pure lambda-calculus formalized for the matita theorem prover F Guidi
Journal of Formalized Reasoning 5 (1), 1-25, 2012
4 2012 Landau’s “Grundlagen der Analysis” from Automath to lambda-delta F Guidi
Tec. Rep. UBLCS 2009-16, Università di Bologna, 2009
4 2009 Lambda types on the lambda 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 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 A formal system for the universal quantification of schematic variables F Guidi
ACM Transactions on Computational Logic (TOCL) 23 (1), 1-37, 2021
1 2021 The Formal System λδ Revised - Stage A: Extending the Applicability Condition F Guidi
arXiv preprint arXiv:1411.0154, 2014
1 2014 
Claudio Sacerdoti CoenUniversity of BolognaEmail verificata su unibo.it