Предавања проф. Марка Безема на Математичком факултету, 22. и 24. јул 2014.

• 21. Јул, 2014
• Коментари (0)

У оквиру посете Групи за аутоматско резоновање, проф. Марк Безем са Универзитета у Бергену, Норвешка, одржаће неколико предавања на тему тренутно веровантно "најврелије" теме логике и рачунарства - хомотопске теорије типова.

Предвиђени термини су уторак 22. и четвртак 24. јула од 16h (на Студентском тргу, вероватно у сали 718), а могући су и додатни часови у среду пре подне и петак пре подне.

Наслов предавања: Homotopy Type Theory

Садржај: Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way.

It is based on a recently discovered connection between homotopy theory and type theory. Homotopy theory is an outgrowth of algebraic topology and homological algebra, with relationships to higher category theory; while type theory is a branch of mathematical logic and theoretical computer science.

Homotopy type theory also brings new ideas into the very foundation of mathematics. For example, there is Voevodsky's subtle and beautiful Univalence Axiom. The univalence axiom implies, in particular, that isomorphic structures can be identified, a principle that mathematicians have been happily using on workdays, despite its incompatibility with the "official" doctrines of conventional foundations.

In the seminar we will focus on type theory for formalizing mathematics and work through (parts of) the HoTT book, freely available from:

http://uf-ias-2012.wikispaces.com/The+book