Группа LtU@Kiev приглашает всех интересующихся теорией языков программирования на наш первый семинар.

Доклады

Введение в системы типов (Андрей Мельников, Киев)

• Исторический обзор развития концепции типов в языках программирования (кратко)
• математические модели функциональных языков программирования (кратко): лямбда исчисление, системы перезаписи термов, системы перезаписи графов
• математические модели систем типов
  • типизация по Карри и по Чёрчу
  • описание систем типов с использованием формальной математики (типы, термы, абстрактный синтаксис, базис, правила вывода)
  • некоторые системы типов на основе лямбда-исчисления (варианты по Чёрчу)
    • simply typed lambda-calculus (функции терм-терм)
    • полиморфное лямбда-исчисление (полиморфные функции, функции тип-терм)
    • лямбда-омега (параметризованные типы, функции тип-тип)
    • лямбда-П (зависимые типы, функции терм-тип)
  • система типов Хиндли-Милнера

Вывод типов и полиморфизм (Роман Чепляка, Одесса)

Доклад посвящён двум важным особенностям многих современных статически типизированных языков программирования.

Полиморфизм позволяет писать функции, не зависящие от типов аргументов, тем самым сокращая объем кода и увеличивая степень его повторного использования.

Вывод типов дает возможность опускать все или многие аннотации типов, делая процесс программирования на статическом языке столь же быстрым и удобным, как и на динамическом, сохраняя в то же время все преимущества статической типизации.

В докладе будут рассмотрены несколько видов параметрического полиморфизма для функциональных языков (предикативный, ML-style, импредикативный) и алгоритмы вывода типов для них.

Динамическая логика и верификация программ (Евгений Беркович, Одесса; Сергей Тропанец, Харьков)

Динамическая логика — это формализм, который позволяет выражать и доказывать свойства программ.

С помощью динамической логики можно:

• проверить, что после выполнения данной программы истинны те или иные условия
• оптимизировать код (доказать эквивалентность данной программы другой, более оптимальной)

и многое другое.

В докладе будет описан язык динамической логики, на котором может быть записана любая программа, а также сформулированы условия корректности её работы. Будут рассмотрены два подхода для проверки корректности: Model Checking и Proving.

Время и место

Суббота, 30 мая 2009 г., 13⁰⁰, G-Club.

Киев, ул. Николая Гринченко, 2/1
+38-044-492-9693
+38-044-492-9695

Регистрация

Для попадания на семинар необходимо зарегистрироваться (желательно — до 26.05) и обязательно иметь при себе документ, удостоверяющий личность (например, паспорт).