RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ЛИЧНЫЙ КАБИНЕТ
Видеотека
Архив
Популярное видео

Поиск
RSS
Новые поступления





Для просмотра файлов Вам могут потребоваться






XVII летняя школа «Современная математика», посвященная памяти Виталия Арнольда, 2017
24 июля 2017 г. 17:15, г. Дубна, дом отдыха «Ратмино»
 


Соответствие Карри–Ховарда: от математической логики к программированию. Занятие 1

В. Н. Брагилевский
Видеозаписи:
MP4 2,743.4 Mb
MP4 623.7 Mb

Количество просмотров:
Эта страница:538
Видеофайлы:270

В. Н. Брагилевский


Видео не загружается в Ваш браузер:
  1. Установите Adobe Flash Player    

  2. Проверьте с Вашим администратором, что из Вашей сети разрешены исходящие соединения на порт 8080
  3. Сообщите администратору портала о данной ошибке

Аннотация: В программировании есть область, тесно связанная с математической логикой и другими разделами математики, — это верификация программного обеспечения, то есть проверка корректности программы относительно некоторой формальной спецификации. В наиболее жёстком режиме верификация превращается в доказательство теорем о правильности результатов работы программ. В этом курсе мы посмотрим на те математические основания, которые делают возможной именно такую верификацию.
Курс начнётся с элементарного введения в интуиционистскую логику и теорию доказательств, в рамках которого мы рассмотрим основные логические связки и правила вывода, а также построение с их помощью деревьев вывода, то есть собственно доказательств. После этого мы перейдём к изучению лямбда-исчисления как модели вычислений (эквивалентной, как известно, машине Тьюринга): мы определим множество лямбда-термов, обсудим понятия подстановки, альфа-эквивалентности и бета-редукции, после чего построим на этой базе простейший язык программирования.
Следующий шаг будет состоять в добавлении к лямбда-исчислению системы типов — так мы получим сначала простое типизированное лямбда-исчисление, а затем и некоторые наиболее важные его расширения. Лямбда-исчисление с типами оказывается удивительным образом связано с теорией доказательств: существует прямая связь между высказываниями и типами, а также между доказательствами и термами (программами) — мы увидим, что «доказывать теорему» означает в точности то же самое, что и «писать программу». Эту связь называют соответствием или изоморфизмом Карри–Ховарда, именно она делает возможными разработку и использование систем автоматического и интерактивного доказательства теорем. Наш курс завершится обзором и небольшой демонстрацией возможностей одной из таких систем, которая называется Coq: с её помощью мы формально докажем одну из математических теорем и построим доказуемо корректную реализацию одного из алгоритмов.
Этот курс не требует предварительных знаний вне стандартной школьной программы по математике и информатике, все используемые в нём понятия будут введены непосредственно по ходу. Курс будет сопровождаться упражнениями.

Website: https://www.mccme.ru/dubna/2017/courses/bragilevsky.html
Цикл лекций

ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru
 
Обратная связь:
 Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2017