В программировании теории языка , то POPLmark вызов (от «Принципов Языки программирования бенчмарка», ранее механизированная Метатеория для масс! ) (Aydemir, 2005) представляет собой набор тестов , предназначенный для оценки состояния автоматизированных рассуждений (или механизации) в метатеория языков программирования, а также для стимулирования обсуждения и сотрудничества среди разнообразных формальных методов.сообщество. Грубо говоря, проблема заключается в измерении того, насколько хорошо программы могут быть доказаны, чтобы соответствовать спецификации того, как они предназначены для поведения (и многих сложных проблем, которые это влечет). Первоначально задача была предложена членами клуба PL при Пенсильванском университете в сотрудничестве с коллегами по всему миру. Практикум по механизированной метатеории является основной встречей исследователей , участвующих в решении задач.
При разработке эталонного теста POPLmark используются общие черты, присущие рассуждениям о языках программирования. Задачи задачи не требуют формализации больших языков программирования, но требуют умения рассуждать о:
- Привязка
- Большинство языков программирования имеют ту или иную форму связывания, варьирующуюся по сложности от простых связывателей просто типизированного лямбда-исчисления до сложных, потенциально бесконечных связывателей, необходимых для обработки шаблонов записей .
- Индукция
- Такие свойства, как редукция предмета и строгая нормализация, часто требуют сложных индукционных аргументов.
- Повторное использование
- Поскольку сотрудничество является ключевой целью этой задачи, ожидается, что решения будут содержать повторно используемые компоненты, которые позволят исследователям обмениваться языковыми функциями и проектами, не требуя от них каждый раз начинать с нуля.
Проблемы
По состоянию на 2007 г.[Обновить], задача POPLmark состоит из трех частей. Часть 1 касается исключительно типов Системы F <: ( Система F с подтипами ) и имеет такие проблемы, как:
- Проверка того, что система типов допускает транзитивность подтипов.
- Проверка транзитивности подтипов при наличии записей
Часть 2 касается синтаксиса и семантики System F <: . Это касается доказательств
- Типовая безопасность для чистого фрагмента
- Безопасность типов при наличии сопоставления с образцом
Часть 3 касается удобства использования формализации системы F <: . В частности, задача требует:
- Моделирование и анимация операционной семантики
- Извлечение полезных алгоритмов из формализации
Было предложено несколько решений по частям проблемы POPLmark с использованием следующих инструментов: Isabelle / HOL , Twelf , Coq , αProlog , ATS , Abella и Matita .
Смотрите также
- Проблема выражения
- Манифест QED
- POPL конференция
Рекомендации
- Брайан Э. Айдемир, Аарон Боханнон, Мэтью Фэйрбэрн, Дж. Натан Фостер, Бенджамин К. Пирс , Питер Сьюэлл , Димитриос Витиниотис, Джеффри Уошберн, Стефани К. Вейрих и Стефан А. Зданцевич. Механизированная метатеория для масс: проблема POPLmark. В доказательстве теорем в логике высокого порядка, 18-я международная конференция, TPHOLs 2005, том 3603 конспектов лекций по информатике, страницы 50–65. Спрингер, Берлин / Гейдельберг / Нью-Йорк, 2005.
- Бенджамин С. Пирс , Питер Сьюэлл , Стефани Вейрих , Стив Зданцевич, Пора механизировать метатеорию языка программирования , В Бертран Мейер, Джим Вудкок (ред.) Проверенное программное обеспечение: теории, инструменты, эксперименты , LNCS 4171, Springer Berlin / Heidelberg, 2008, стр. 26–30, ISBN 978-3-540-69147-1