POPLmark вызов

В теории языков программирования тест POPLmark (из «Принципов языков программирования», ранее называвшийся «Механизированная метатеория для масс!» ) (Aydemir, 2005) представляет собой набор тестов , предназначенных для оценки состояния автоматизированных рассуждений (или механизации) в метатеорию языков программирования, а также стимулировать дискуссии и сотрудничество среди различных слоев сообщества формальных методов . Грубо говоря, задача состоит в том, чтобы измерить, насколько хорошо программы могут соответствовать спецификациям того, как они должны вести себя (и во многих сложных вопросах, которые с этим связаны). Первоначально задача была предложена членами клуба PL совместно Пенсильванского университета с коллегами по всему миру. Семинар по механизированной метатеории — это основная встреча исследователей, участвующих в проекте.

При разработке теста POPLmark учитываются особенности, общие для рассуждений о языках программирования. Сложные задачи не требуют формализации больших языков программирования, но требуют сложности рассуждений о:

Связывание: Большинство языков программирования имеют ту или иную форму привязки, варьирующуюся по сложности от простых связок просто типизированного лямбда-исчисления до сложных, потенциально бесконечных связок, необходимых для обработки записей шаблонов .
Индукция: Такие свойства, как редукция субъекта и сильная нормализация, часто требуют сложных аргументов индукции.
повторное использование: Поскольку ключевой целью задачи является развитие сотрудничества, ожидается, что решения будут содержать повторно используемые компоненты, которые позволят исследователям обмениваться языковыми функциями и конструкциями, не требуя от них каждый раз начинать с нуля.

Проблемы [ править ]

По состоянию на 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

Внешние ссылки [ править ]

Вызов POPLmark