Predavanja prof. Marka Bezema na Matematičkom fakultetu, 22. i 24. jul 2014.

U okviru posete Grupi za automatsko rezonovanje, prof. Mark Bezem sa Univerziteta u Bergenu, Norveška, održaće nekoliko predavanja na temu trenutno verovantno "najvrelije" teme logike i računarstva - homotopske teorije tipova.

Predviđeni termini su utorak 22. i četvrtak 24. jula od 16h (na Studentskom trgu, verovatno u sali 718), a mogući su i dodatni časovi u sredu pre podne i petak pre podne.

Naslov predavanja: Homotopy Type Theory

Sadržaj: 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



Ostavite vaš komentar:


(opciono)
(nece biti prikazano)