ALF (помощник корректора)
ALF («Другая логическая структура») — это редактор структур для мономорфной теории типов Мартина-Лёфа , разработанный в Университете Чалмерса . Он является предшественником помощников доказательства Alfa, Agda , Cayenne и Coq и языков программирования с зависимой типизацией . Это был первый язык, поддерживающий индуктивные семейства и зависимое сопоставление с образцом. [1] [2]
Ссылки
- ^ Тьерри Кокван (1992). «Соответствие шаблону с зависимыми типами». В Бенгте Нордстреме, Кенте Петерссоне и Гордоне Плоткине (редакторы), Электронные труды третьего ежегодного семинара BRA по логическим структурам (Бостад, Швеция) .
- ^ Торстен Альтенкирх , Конор Макбрайд и Джеймс Маккинна (2005). «Почему зависимые типы имеют значение».
Дальнейшее чтение
- Лена Магнуссон и Бенгт Нордстрём. «Редактор корректуры ALF и его корректурный движок».
- Торстен Альтенкирх , Вероника Гаспес, Бенгт Нордстрем и Бьорн фон Сюдов. «Руководство пользователя по ALF».
Внешние ссылки
- Альфа
 | Эта статья по информатике — заглушка . Вы можете помочь Википедии, расширив ее. |
