Metodi Matematici per Informatica e Seminario Studenti PhD

Verona - dicembre 2011 - gennaio 2012
e dicembre 2012 - gennaio 2013

  • Letture:

  • Argomenti corso:
Esame scritto: E` possibile, come opzione, sostenere un esame scritto anche sugli argomenti di teoria della dimostrazione, lambda calcolo e categorie invece che fare una presentazione orale.
Presentazioni studenti per credito:
  • Categorie cartesiane chiuse presentate equazionalmente e sistemi di Gentzen:
    Lambek e Scott: Introduction to higher order categorical logic Part 0-1
    Tom Leinster's Courses Category theory 2007-8
  • 1. Categorie cartesiane, regole della congiunzione nella deduzione naturale e nel calcolo dei sequenti; corrispondenze sintattiche, normalizzazione ed eliminzione del taglio.
  • 2. Categorie cartesiane chiuse, regole dell'implicazione nella deduzione naturale e nel calcolo dei sequenti; corrispondenze sintattiche, normalizzazione ed eliminzione del taglio.
  • 3. Categorie bicartesiane, regole della disgiunzione nella deduzione naturale e nel calcolo dei sequenti; corrispondenze sintattiche, normalizzazione ed eliminzione del taglio.
  • 4. Le categorie bicartesiane chiuse sono degenerate
  • 5. Nella categoria Sets il coesponsnte e` degenerato (T.Crolard Substractive Logic)
  • 6. Categorie monoidali chiuse. Definizione e confronto con le CCC.
  • 7. Definizione di una coategoria monoidale come invariante della normalizzazione dalla logica lineare intuizionistica
  • 8. Il teorema di coerenza nelle categorie monoidali (McLane Categories for the working mathematician)