Telegram Group & Telegram Channel
#матлог #не_мехмат

В ближайшие две среды, 9 и 16 апреля 2025 г., С.Л. Кузнецов прочитает две лекции в рамках курса «Coq» в Центральном университете.

Первая лекция будет посвящена вычислительным возможностям различных версий лямбда-исчисления. Будет рассказано, что в бестиповом лямбда-исчислении представимы все вычислимые функции, а также охарактеризованы подклассы всюду определённых вычислимых функций, представимых в простом типовом лямбда-исчислении и лямбда-исчислении второго порядка (система F).

На второй лекции будет рассказано о доказательстве непротиворечивости исчисления индуктивных конструкций (CIC — базовое исчисление системы Coq) в рамках теории множеств ZFC со счётным набором недостижимых кардиналов, а также обратное кодирование соответствующих расширений ZFC в Coq, по статье Б. Вернера 1997 г.

Место: учебный корпус Центрального университета, Москва, ул. Гашека, д. 7, аудитория F304 (3 этаж, из лифтов перейти по мосту и прямо)
Время: 9 и 16 апреля, 19:30

Для посещения нужно получить пропуск. Для этого нужно написать в телеграм Владу Пимкину @delamelicon, что идёте на лекцию С.Л.Кузнецова в среду. Желательно сделать это не позднее вторника.

ВК
🔥5👍2



group-telegram.com/msu_mathlog/192
Create:
Last Update:

#матлог #не_мехмат

В ближайшие две среды, 9 и 16 апреля 2025 г., С.Л. Кузнецов прочитает две лекции в рамках курса «Coq» в Центральном университете.

Первая лекция будет посвящена вычислительным возможностям различных версий лямбда-исчисления. Будет рассказано, что в бестиповом лямбда-исчислении представимы все вычислимые функции, а также охарактеризованы подклассы всюду определённых вычислимых функций, представимых в простом типовом лямбда-исчислении и лямбда-исчислении второго порядка (система F).

На второй лекции будет рассказано о доказательстве непротиворечивости исчисления индуктивных конструкций (CIC — базовое исчисление системы Coq) в рамках теории множеств ZFC со счётным набором недостижимых кардиналов, а также обратное кодирование соответствующих расширений ZFC в Coq, по статье Б. Вернера 1997 г.

Место: учебный корпус Центрального университета, Москва, ул. Гашека, д. 7, аудитория F304 (3 этаж, из лифтов перейти по мосту и прямо)
Время: 9 и 16 апреля, 19:30

Для посещения нужно получить пропуск. Для этого нужно написать в телеграм Владу Пимкину @delamelicon, что идёте на лекцию С.Л.Кузнецова в среду. Желательно сделать это не позднее вторника.

ВК

BY Кафедра математической логики и теории алгоритмов мехмата МГУ


Warning: Undefined variable $i in /var/www/group-telegram/post.php on line 260

Share with your friend now:
group-telegram.com/msu_mathlog/192

View MORE
Open in Telegram


Telegram | DID YOU KNOW?

Date: |

What distinguishes the app from competitors is its use of what's known as channels: Public or private feeds of photos and videos that can be set up by one person or an organization. The channels have become popular with on-the-ground journalists, aid workers and Ukrainian President Volodymyr Zelenskyy, who broadcasts on a Telegram channel. The channels can be followed by an unlimited number of people. Unlike Facebook, Twitter and other popular social networks, there is no advertising on Telegram and the flow of information is not driven by an algorithm. "The inflation fire was already hot and now with war-driven inflation added to the mix, it will grow even hotter, setting off a scramble by the world’s central banks to pull back their stimulus earlier than expected," Chris Rupkey, chief economist at FWDBONDS, wrote in an email. "A spike in inflation rates has preceded economic recessions historically and this time prices have soared to levels that once again pose a threat to growth." "And that set off kind of a battle royale for control of the platform that Durov eventually lost," said Nathalie Maréchal of the Washington advocacy group Ranking Digital Rights. Stocks dropped on Friday afternoon, as gains made earlier in the day on hopes for diplomatic progress between Russia and Ukraine turned to losses. Technology stocks were hit particularly hard by higher bond yields. Some privacy experts say Telegram is not secure enough
from us


Telegram Кафедра математической логики и теории алгоритмов мехмата МГУ
FROM American