- F. Guidi, C. 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.

- F. 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.

- F. 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.

- F. 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.

- F. 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.

- A. Asperti, L. Padovani, C. Sacerdoti Coen, F. Guidi, I. Schena:
**Mathematical Knowledge Management in HELM**. In*Annals of Mathematics and Artificial Intelligence*38(1-3), Kluwer Academic Publishers (May 2003), pp. 27-46.

- C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. 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.

- F. Guidi, C. 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*.

- A. Asperti, F. 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.

- A. Asperti, F. Guidi, C. Sacerdoti Coen, E. Tassi, S. 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.

- F. Guidi, C. 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.

- F. Guidi, I. 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.

- F. Guidi, C. Sacerdoti Coen, E. 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), article n. 8. HAL Id: hal-01410567.

- F. 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.

- F. 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.

- F. 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.

- F. Guidi, C. 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.

- A. Asperti, L. Padovani, C. Sacerdoti Coen, F. Guidi, I. Schena:
**Mathematical Knowledge Management in HELM**. In local proc. of 1st International Workshop on Mathematical Knowledge Management (MKM 2001). University of Linz (September 2001), article n. 3.

- F. Guidi:
**Extending the Applicability Condition in the Formal System λδ**. Technical report AMS Acta 4411, University of Bologna (December 2015).

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

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

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

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

- F. 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).

- F. 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).

- F.Guidi:
**A Note on Basic Implication**. Preprint (March 2002).

- F. Guidi:
**lambdadelta_2A1**. Computer-checked formal specification. <http://lambdadelta.info/> (August 2015).

- F. Guidi:
**lambdadelta_1**. Computer-checked formal specification. <http://lambdadelta.info/> (May 2008).

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

Last update: Wed, 11 Jan 2017 16:24:13 +0100