Задача POPLmark - Википедия - POPLmark challenge

Эта статья поднимает множество проблем. Пожалуйста помоги Улучши это или обсудите эти вопросы на страница обсуждения. (Узнайте, как и когда удалить эти сообщения-шаблоны) Эта статья нужны дополнительные цитаты для проверка. Пожалуйста помоги улучшить эту статью к добавление цитат в надежные источники. Материал, не полученный от источника, может быть оспорен и удален Найдите источники: «Вызов POPLmark»  – Новости  · газеты  · книги  · ученый  · JSTOR (Январь 2011 г.) (Узнайте, как и когда удалить этот шаблон сообщения) Эта статья включает Список ссылок, связанное чтение или внешняя ссылка, но его источники остаются неясными, потому что в нем отсутствует встроенные цитаты. Пожалуйста, помогите улучшать эта статья введение более точные цитаты. (Январь 2011 г.) (Узнайте, как и когда удалить этот шаблон сообщения) (Узнайте, как и когда удалить этот шаблон сообщения)

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

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

Привязка

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

Индукция

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

Повторное использование

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

Проблемы

Этот раздел должен быть обновлено. Обновите эту статью, чтобы отразить недавние события или новую доступную информацию. (Март 2020 г.)

По состоянию на 2007 год^{[Обновить]}, задача POPLmark состоит из трех частей. Часть 1 касается исключительно типов Система F_<: (Система F с подтип ) и имеет такие проблемы, как:

1. Проверка того, что система типов допускает транзитивность подтипов.
2. Проверка транзитивности подтипов при наличии записи

Часть 2 касается синтаксиса и семантики System F_<:. Это касается доказательств

1. Безопасность типов для чистого фрагмента
2. Безопасность типов при наличии сопоставление с образцом

Часть 3 касается удобства использования формализации Системы F._<:. В частности, задача требует:

1. Моделирование и анимация операционная семантика
2. Извлечение полезных алгоритмов из формализации

Было предложено несколько решений по частям проблемы POPLmark с использованием следующих инструментов: Изабель / ХОЛ, Двенадцать, Coq, αProlog, АТС, Абелла и Матита.

Смотрите также

• Проблема выражения
• Манифест QED
• POPL конференция

Рекомендации

• Брайан Э. Айдемир, Аарон Боханнон, Мэтью Фэйрбэрн, Дж. Натан Фостер, Бенджамин С. Пирс, Питер Сьюэлл, Димитриос Витиниотис, Джеффри Вашберн, Стефани К. Вейрих, и Стефан А. Зданцевич. Механизированная метатеория для масс: проблема POPLmark. В доказательстве теорем в логике высокого порядка, 18-я Международная конференция, TPHOLs 2005, том 3603 конспектов лекций по информатике, страницы 50–65. Шпрингер, Берлин / Гейдельберг / Нью-Йорк, 2005.

• Бенджамин С. Пирс, Питер Сьюэлл, Стефани Вейрих, Стив Зданцевич, Пришло время механизировать метатеорию языков программирования, В книге Бертрана Мейера, Джима Вудкока (ред.) Проверенное программное обеспечение: теории, инструменты, эксперименты, LNCS 4171, Springer Berlin / Heidelberg, 2008 г., стр. 26–30, ISBN  978-3-540-69147-1

внешняя ссылка

• Задача POPLmark

Этот Информатика статья - это заглушка. Вы можете помочь Википедии расширяя это.

Этот язык программирования -связанная статья является заглушка. Вы можете помочь Википедии расширяя это.