В теории языков программирования , задача POPLmark (от "Principles of Programming Languages benchmark", ранее Mechanized Metatheory for the Masses! ) (Aydemir, 2005) представляет собой набор контрольных показателей, разработанных для оценки состояния автоматизированного рассуждения (или механизации) в метатеории языков программирования и для стимулирования обсуждения и сотрудничества среди различных слоев сообщества формальных методов . Очень грубо говоря, задача заключается в измерении того, насколько хорошо программы могут соответствовать спецификации того, как они должны себя вести (и много сложных вопросов, которые это включает). Задача была первоначально предложена членами клуба PL в Университете Пенсильвании совместно с соавторами по всему миру. Workshop on Mechanized Metatheory является основной встречей исследователей, участвующих в задаче.
Дизайн бенчмарка POPLmark руководствуется особенностями, общими для рассуждений о языках программирования. Задачи-вызовы не требуют формализации больших языков программирования, но они требуют сложности в рассуждениях о:
- Связывание
- Большинство языков программирования имеют некоторую форму связывания, варьирующуюся по сложности от простых связывателей простого типизированного лямбда-исчисления до сложных, потенциально бесконечных связывателей, необходимых при обработке шаблонов записей .
- Индукция
- Такие свойства, как редукция субъекта и сильная нормализация, часто требуют сложных индукционных аргументов.
- Повторное использование
- Поскольку ключевой целью конкурса является развитие сотрудничества, ожидается, что решения будут содержать повторно используемые компоненты, которые позволят исследователям обмениваться языковыми функциями и разработками, не требуя от них каждый раз начинать с нуля.
Проблемы
По состоянию на 2007 год [update], задача POPLmark состоит из трех частей. Часть 1 касается исключительно типов System F <: ( System F с подтипированием ) и имеет такие проблемы, как:
- Проверка того, что система типов допускает транзитивность подтипирования.
- Проверка транзитивности подтипирования при наличии записей
Часть 2 касается синтаксиса и семантики Системы F <: . Она касается доказательств
- Типобезопасность для чистого фрагмента
- Безопасность типов при наличии сопоставления с образцом
Часть 3 касается удобства использования формализации Системы F <: . В частности, задача требует:
- Моделирование и анимация операционной семантики
- Извлечение полезных алгоритмов из формализации
Было предложено несколько решений для частей задачи POPLmark с использованием следующих инструментов: Isabelle/HOL , Twelf , Coq , αProlog, ATS , Abella и Matita .
Смотрите также
Ссылки
- Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce , Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie C. Weirich и Stephan A. Zdancewic. Механизированная метатеория для масс: вызов POPLmark. В Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, том 3603 Lecture Notes in Computer Science, страницы 50–65. Springer, Берлин/Гейдельберг/Нью-Йорк, 2005.
- Бенджамин К. Пирс , Питер Сьюэлл, Стефани Вайрих , Стив Зданцевич, «Пора механизировать метатеорию языков программирования» , в книге Бертрана Мейера, Джима Вудкока (ред.) «Проверенное программное обеспечение: теории, инструменты, эксперименты» , LNCS 4171, Springer Berlin / Heidelberg, 2008, стр. 26–30, ISBN 978-3-540-69147-1
Внешние ссылки
