Уважаемые коллеги! Приглашаем принять участие в заседаниях семинара! 

В среду 24 мая выступит Николай Дмитриевич Кудасов (Университет Иннополис): Rzk Proof Assistant and Simplicial HoTT Formalisation.

Аннотация: Rzk is an experimental proof assistant for synthetic infinity-categories. This project has started with the idea of bringing Riehl and Shulman's 2017 to "life" by implementing a proof assistant based on their type theory with shapes. An early prototype with an online playground is available. Perhaps, the largest formalizations are available in two related projects done in collaboration with Emily Riehl and Jonathan.

Weinberger: https://github.com/fizruk/sHoTT and https://github.com/emilyriehl/yoneda. In this talk, I will introduce the proof assistant, demonstrate some of its features, and briefly go over available formalizations. (Early prototype of a proof assistant is available.)
Заседание пройдет гибридно - в аудитории 422 Университета Иннополис и онлайн в Skype (https://join.skype.com/DOsdMMwFpqsm, можно смотреть в браузере)​​ с 14:30 до 16:00 московского времени (18:30-20:00 в Барнауле и Новосибирске).
 
В пятницу 26 мая выступит Ольга Авенировна Невзорова (Казанский федеральный университет): Образовательная онтология ONTOMATH: проблемы онтологического инжиниринга (см. аннотацию на странице семинара https://persons.iis.nsk.su/en/STEP-2023). Заседание пройдет тоже гибридно - в Казанском Федеральном Университете и онлайн в Skype​​​ с 14:30 до 16:00 московского времени (18:30-20:00 в Барнауле и Новосибирске).