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