Agda - это типизированный, полностью функциональный язык программирования и помощник по проверке.
Agda - это типизированный язык программирования с зависимой типизацией. Он имеет индуктивные семейства, то есть типы данных, которые зависят от значений, таких как тип векторов заданной длины. Он также имеет параметризованные модули, операторы mixfix, символы Unicode и интерактивный интерфейс Emacs, который может помочь программисту в написании программы.
Агда - помощник по проверке. Это интерактивная система для написания и проверки доказательств. Agda основана на интуиционистской теории типов, основополагающей системе конструктивной математики, разработанной шведским логиком Пером Мартином-Лёфом. Он имеет много общего с другими помощниками по доказательству, основанными на зависимых типах, таких как Coq, Epigram, Matita и NuPRL.
Текущая версия 2.5.3