Μάθημα : Ειδικά Θέματα Λογικής: Θεωρία Τύπων

Επαγωγικοί τύποι και αναδρομή

• Ο τύπος τών φυσικών αριθμών
• Αναδρομή στούς φυσικούς αριθμούς
• Άλλα παραδείγματα επαγωγικών τύπων

Κατασκευαστική λογική

• Η ερμηνεία Brouwer-Heyting-Kolmogorov
• Φυσική απαγωγή
• Propositions-as-types

Ισότητα

Επαγωγή

Σύμπαντα

Η ιεραρχία τών τύπων ισότητας

Ανώτεροι επαγωγικοί τύποι και univalence

Propositional resizing and topos logic

Μαθηματικά στήν Ομοτοπική Θεωρία Τύπων / Η Ομοτοπική Θεωρία Τύπων ως θεμέλιο τών κατασκευαστικών-στρουκτουραλιστικών μαθηματικών (θεωρία ομοτοπίας, θεωρία κατηγοριών, θεωρία συνόλων)

Εισαγωγή στήν Agda

Δια ζώσης διδασκαλία

Εβδομαδιαίες ασκήσεις

Προετοιμασία και παρουσίαση θέματος τής επιλογής τού φοιτητή, από λίστα θεμάτων ή μετά από συνεννόηση με τόν διδάσκοντα.

The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013.

Egbert Rijke, Introduction to Homotopy Type Theory (2022).

Νίκος Ρήγας

nicolasr@di.uoa.gr