Английская Википедия:ALF (proof assistant)

Материал из Онлайн справочника
Версия от 02:44, 27 декабря 2023; EducationBot (обсуждение | вклад) (Новая страница: «{{Английская Википедия/Панель перехода}} {{Short description|Structure editor for monomorphic Martin-Löf type theory}} {{for|the programming language|Algebraic Logic Functional programming language}} '''ALF''' ("Another logical framework") is a structure editor for monomorphic Martin-Löf type theory developed at Chalmers University. It is a predecessor of the Alfa, Agda (programming lang...»)
(разн.) ← Предыдущая версия | Текущая версия (разн.) | Следующая версия → (разн.)
Перейти к навигацииПерейти к поиску

Шаблон:Short description Шаблон:For ALF ("Another logical framework") is a structure editor for monomorphic Martin-Löf type theory developed at Chalmers University. It is a predecessor of the Alfa, Agda, Cayenne and Coq proof assistants and dependently typed programming languages. It was the first language to support inductive families and dependent pattern matching.[1][2]

References

Шаблон:Reflist

Further reading

External links

Шаблон:Comp-sci-stub

Партнерские ресурсы
Криптовалюты
Магазины
Хостинг
Разное

  1. ↑ Thierry Coquand (1992). "Pattern Matching with Dependent Types". In Bengt Nordström, Kent Petersson, and Gordon Plotkin (editors), Electronic Proceedings of the Third Annual BRA Workshop on Logical Frameworks (Båstad, Sweden).
  2. ↑ Thorsten Altenkirch, Conor McBride and James McKinna (2005). "Why Dependent Types Matter".
Источник — http://wikihandbk.com/ruwiki/index.php?title=Английская_Википедия:ALF_(proof_assistant)&oldid=12882030