προωθημένο από Αναστάσιο Φράγκο..
-----------------------------------
Καλησπέρα σε όλους!
Την ερχόμενη Τρίτη 01/04 και ώρα 13.00 θα έχουμε το δεύτερο μέρος της
παρουσίασης του Ανδρέα. Μας άρεσε και θέλαμε συνέχεια.
Παρεμπιπτόντως, οι σημειώσεις των διαλέξεων έχουν ανέβει στην σελίδα!
Link!
https://afragos-math.github.io/seminars/gradclubfiles/s2024-25/aavoukatos(HoTT).html
Τίτλος: An Introduction to Martin-Löf Type Theory: A Constructive Approach
to Mathematics and Computation
Συντεταγμένες: Τρίτη 01/04, ώρα 13.00-14.00, αίθουσα Α31
Ομιλητής: Ανδρέας Αβουκάτος
Περίληψη: Martin-Löf Type Theory (MLTT) provides a constructive foundation
for mathematics and computation, integrating logic and type theory in a
unified framework. This talk introduces the core principles of MLTT,
including dependent types, inductive types, and identity types. We explore
how MLTT serves as a foundation for constructive mathematics and
influences proof assistants such as Agda. Additionally, we discuss its
role in formalising mathematics and its extension in Homotopy Type Theory
(HoTT). The talk assumes basic familiarity with mathematical reasoning but
does not require prior knowledge of type theory.
