Ferruccio Guidi

My Contacts

• EMail: username@cs.unibo.it (replace username with fguidi).

• Home address: Cannaregio 1104 Venezia I-30121 Italy. Here is a map showing the location.

• University address: via Malaguti 1 (office 13) Bologna I-40127 Italy. Here is a map showing the location.
  

My Curriculum

• PhD in Computer Science at Università di Bologna (advisor: Prof. A. Asperti).

• Degree in Mathematics at Università di Padova (advisor: Prof. G. Sambin).

My Main Research Interests

• Currently (at the HELM Working Group): computer assisted theorem proving, type theory, lambda calculus.

• Formerly  (at the Mathematical Logic Research Group in Padua): Basic Logic, predicative topology.
  

My Papers

• Here is the complete list of my publications. Here is my DBLP entry.
  

• Here is my graduation thesis (58 pages, in Italian) defended at Università di Padova:
  F. Guidi: Il terzo teorema di Gödel-Kreisel nella teoria intuizionistica dei tipi di Martin-Löf.
  It contains a proof of the third Gödel-Kreisel theorem and the tools to formalise it in Martin-Löf CTT, it also contains a simple syntactic proof of Herbrand's theorem for negated prenex formulae in intuitionistic logic.

My Developments

• λδ (lambda-delta): a typed lambda calculus that pursues the reuse of the term constructions both at the level of types and at the level of contexts, while enjoying the most common meta-theoretical properties.

• Procedural Reconstruction: a feature of the formal proof management system Matita.
  

• MathQL-1: a query language for RDF meta-data developed in the context of the project HELM.

• Integer sequences registered in the OEIS: A155504, A155751, A155754, A157449.

• inference.sty (2009-01-08): a LaTeX package with facilities for typesetting trees of inference rules. Instructions will appear soon.
  

My Teaching (in Italian)

• Assistenza al Corso di Programmazione 2000-2001 (Prof. C. Laneve)

  Esercizi su O, Omega e Theta: oot_s.pdf (36 pagine)
  lucidi da 0 a 9: funzioni non ricorrenti (lezione del 15-12-2000)
  lucidi da 10 a 23: funzioni ricorrenti (lezioni del 30,31-01-2001)
  lucidi da 24 a 35: esercizi di ricapitolazione (lezione del 09-03-2001)

  Esercizi sui sistemi di transizione: sop_s.pdf (28 pagine)
  lucidi da 0 a 3 (lezione del 11-05-2001)
  lucidi da 4 a 15 (lezione del 25-05-2001)
  lucidi da 16 a 27 (lezione aggiuntiva del 29-05-2001)

• Ricevimento studenti: su appuntamento da richiedere tramite e-mail (indicata sopra).