Ferruccio Guidi

My Contacts

• EMail: name@unibo.it (replace name with ferruccio.guidi).

• Home address: Cannaregio 1104, Venezia 30121, Italy. Here is a map showing the location (the map reports "Cannaregio 104" by mistake).

• University address: via Antonio Zanolini 41 (rear entrance, first floor, open space), Bologna 40126, Italy. Here is a map showing the location.

My Current Position

• Teaching assistant for the course "logical basis of computer science" at DISI, Università di Bologna (advisor: C. Sacerdoti Coen).

My Curriculum

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

• Degree in Mathematics at Università di Padova (advisor: 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 profile at Google Scholar. 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.

• Here are my novels (in Italian)

  

My Developments

• λδ (\lambda\delta) (first mirror) (second mirror): a family of typed lambda calculi that pursue the reuse of the term constructions both at the level of types and at the level of local environments, 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 (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).

My Favorite Quotes

• "Arguing is part of understanding." (Crenelyn Emboltorio, private communication)

• "We, the people of Moonbase Alpha, did exist." (Zienia Merton as Sandra Benes, Message from Moonbase Alpha)

• "Answers are needed to some questions." (Ed Bishop as Edward Straker, UFO episode 1)

• "Your existence is a contradiction." (Fuyuka Ōura as Lady Lambdadelta, Umineko no Naku Koro ni)

• "My logic is undeniable." (Fiona Hogan as VIKI, I, Robot)

• "Desertion is not an option." (Julianne Moore as ARIIA, Eagle Eye)

• "Io spero di dire di lei quello che mai non fue detto d’alcuna." (Dante Alighieri, Vita Nuova)
  

• "And yet, and yet. Who knows the end?" (Ayesha, Wisdom's Daughter)