Byla vydána Agda verze 2.6.3. Přináší o 30% rychlejší typovou kontrolu (měřeno na standardní knihovně) a širší podporu reflexe (generování typů).
Agda je funkcionální jazyk s typovým systémem, který umožňuje také formální verifikaci algoritmů a obecněji formalizaci důkazů matematických tvrzení. Patří tak do stejné skupiny jazyků jako Coq, Isabelle, ATS, Lean a Idris. V současné době má backend pro Haskell a JavaScript.
ČLÁNKY DO MAILU