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