Ferruccio Guidi - Publications

In Preparation

• Ferruccio Guidi, Rob Nederpelt: A new name-free system of lambda calculus with delayed updating. In preparation.

• Ferruccio Guidi: Updating References by Depth in Lambda Calculus. In preparation.

Journal Articles

• Ferruccio Guidi: A Formal System for the Universal Quantification of Schematic Variables. In Transactions on Computational Logic 23(1), ACM (January 2022), pp 2:1-2:37. CoRR Id: arXiv:1911.12749.

• Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi: Implementing type theory in higher order constraint logic programming. In Mathematical Structures in Computer Science 29(8), special issue on Structural Proof Theory, Automated Reasoning and Computation in Celebration of Dale Miller’s 60th Birthday, Cambridge University Press (September 2019), pp. 1125-1150.

• Ferruccio Guidi, Claudio Sacerdoti Coen: A Survey on Retrieval of Mathematical Knowledge. In Mathematics in Computer Science 10(4), Birkhäuser Science, Springer (December 2016), pp. 409-427.

• Ferruccio Guidi: Verified Representations of Landau's "Grundlagen" in the λδ Family and in the Calculus of Constructions. In Journal of Formalized Reasoning 8(1), University of Bologna (December 2015), pp. 93-116.

• Ferruccio Guidi: Standardization and Confluence in Pure λ-Calculus Formalized for the Matita Theorem Prover. In Journal of Formalized Reasoning 5(1), University of Bologna (December 2012), pp. 1-25.

• Ferruccio Guidi: Procedural Representation of CIC Proof Terms. In Journal of Automated Reasoning 44(1-2), special issue on Programming Languages for Mechanized Mathematics Systems, Springer (February 2010), pp. 53-78.

• Ferruccio Guidi: The Formal System λδ. In Transactions on Computational Logic 11(1), ACM (October 2009), pp. 5:1-5:37 and online appendix pp. 1-11. CoRR Id: arXiv:cs/0611040.

• Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Ferruccio Guidi, Irene Schena: Mathematical Knowledge Management in HELM. In Annals of Mathematics and Artificial Intelligence 38(1-3), Kluwer Academic Publishers (May 2003), pp. 27-46.

Conference Articles

• Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi: ELPI: Fast, Embeddable, λProlog Interpreter. In proc. of 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 20). Lecture Notes in Computer Science 9450, Springer (December 2015), pp. 460-468. HAL Id: hal-01176856.

• Ferruccio Guidi, Claudio Sacerdoti Coen: A Survey on Retrieval of Mathematical Knowledge. In proc. of 8th Conference on Intelligent Computer Mathematics (CICM 2015). Lecture Notes in Artificial Intelligence 9150, Springer (July 2015), pp. 296-315. CoRR Id: arXiv:1505.06646. Best paper in the Projects and Surveys track.

• Andrea Asperti, Ferruccio Guidi: Type Systems for Dummies. In proc. of 7th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2012). ACM (January 2012), pp. 79-90.

• Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli: A Content Based Mathematical Search Engine: Whelp. In proc. of Types for Proofs and Programs: International Workshop (Types 2004). Lecture Notes in Computer Science 3839, Springer (January 2006), pp. 17-32.

• Ferruccio Guidi, Claudio Sacerdoti Coen: Querying Distributed Digital Libraries of Mathematics. In proc. of 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2003). Aracne (September 2003), pp. 17-30.

• Ferruccio Guidi, Irene Schena: A Query Language for a Metadata Framework about Mathematical Resources. In proc. of 2nd International Conference on Mathematical Knowledge Management (MKM 2003). Lecture Notes in Computer Science 2594, Springer (February 2003), pp. 105-118.

Contributions to Local Proceedings

• Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi: Implementing Type Theory in Higher Order Constraint Logic Programming. In local proc. of Event Celebrating Professor Dale Miller's 60th Birthday (FDM 2016). Université Paris-VII (December 2016), pp. 8:1-8:21. HAL Id: hal-01410567.

• Ferruccio Guidi: An Efficient Validation Procedure for the Formal System λδ. In local proc. of 6th Conference on Computability in Europe (CiE 2010). CMATI Booklet, Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores (July 2010), pp. 204-213.

• Ferruccio Guidi: Procedural Representation of CIC Proof Terms. In local proc. of Programming Languages for Mechanized Mathematics Workshop (PLMMS 2007). RISC Report Series 07-10 (3120), University of Linz (June 2007), pp. 36-52.

• Ferruccio Guidi: Lambda Types on the Lambda Calculus with Abbreviations. In local proc. of 3rd Conference on Computability in Europe (CiE 2007). Quaderni del Dipartimento di Scienze Matematiche e Informatiche "Roberto Magari" ID 487, University of Siena (June 2007), p. 387.

• Ferruccio Guidi, Claudio Sacerdoti Coen: Querying Distributed Digital Libraries of Mathematics. In local proc. of Calculemus 2003 conference. Technical report LIP6 2003/010, Laboratoire D'Informatique de Paris 6 (September 2003), pp. 17-30.

• Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Ferruccio Guidi, Irene Schena: Mathematical Knowledge Management in HELM. In local proc. of 1st International Workshop on Mathematical Knowledge Management (MKM 2001). University of Linz (September 2001), pp. 3:1-3:21.

Technical Reports

• Ferruccio Guidi: The Formal System λΥP. Technical report AMS Acta 5754, University of Bologna (December 2017).

• Ferruccio Guidi: Extending the Applicability Condition in the Formal System λδ. Technical report AMS Acta 4411, University of Bologna (December 2015). CoRR Id: arXiv:1411.0154.

• Ferruccio Guidi: Landau's "Grundlagen der Analysis" from Automath to lambda-delta. Technical report UBLCS 2009-16, University of Bologna (September 2009).

• Ferruccio Guidi: A Note on Basic Implication. Technical report UBLCS 2009-01, University of Bologna (January 2009).

• Ferruccio Guidi: Lambda-Types on the Lambda-Calculus with Abbreviations. Technical report UBLCS 2006-25, University of Bologna (November 2006).

• Ferruccio Guidi: Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification. Technical report UBLCS 2006-01, University of Bologna (January 2006).

• Ferruccio Guidi: Searching and Retrieving in Content-based Repositories of Formal Mathematical Knowledge. Ph.D. Thesis in Computer Science. AMS Tesi di Dottorato 7197 and technical report UBLCS 2003-06, University of Bologna (March 2003).

• Ferruccio Guidi: Il terzo teorema di Gödel-Kreisel nella teoria intuizionistica dei tipi di Martin-Löf. Graduation Thesis in Mathematics. PAdova Digital University Archive 27030, University of Padova (July 1998).

Preprints

• Ferruccio Guidi: A Note on Basic Implication. Preprint (March 2002). Superseded by technical report UBLCS 2009-01.

Formal Specifications in Digital Format

• Ferruccio Guidi: lambdadelta_2B. Computer-checked formal specification. <http://lambdadelta.info/> (November 2019).

• Ferruccio Guidi: lambdadelta_2A. Computer-checked formal specification. <http://lambdadelta.info/> (August 2015).

• Ferruccio Guidi: lambdadelta_1A. Computer-checked formal specification. <http://lambdadelta.info/> (May 2008).

• Ferruccio Guidi: Subset Theory on an Intuitionistic and Predicative Foundation. Computer-checked formal specification. <http://www.cs.unibo.it/~fguidi/download/SUBSETS.tgz> (June 2005).