Agda | ||||
---|---|---|---|---|
Paradigma | zuiver functioneel programmeren | |||
Verschenen | 2007 (16 jaar) | |||
Ontworpen door | Ulf Norell, Catarina Coquand | |||
Ontwikkeld door | Ulf Norell, Catarina Coquand | |||
Huidige versie | 2.7.0.1 (12 september 2024)[1] | |||
Typesysteem | sterke typering, manifest typering, afhankelijke typering, statisch typesysteem, nominatief typesysteem, type-inferentie | |||
Beïnvloed door | Coq, Epigram, Haskell | |||
Invloed op | Idris (programmeertaal) | |||
Besturingssysteem | Platform-onafhankelijke software | |||
Licentie | BSD-licentie | |||
Bestandsextensies | agda , lagda
| |||
Website | (en) Projectpagina | |||
|
Agda is een afhankelijk getypeerde functionele programmeertaal, oorspronkelijk ontwikkeld door Ulf Norell aan de Technische Universiteit Chalmers. Agda is niet Turingvolledig.
Agda is een bewijsassistent gebaseerd op het propositions-as-types paradigma, maar heeft in tegenstelling tot Coq geen aparte tactiektaal. Bewijzen worden geschreven in een functionele programmeerstijl. De taal heeft gebruikelijke programmeerconstructies zoals datatypes, pattern matching, records, let expressies en modules, en een Haskell-achtige syntaxis. Het systeem heeft interfaces voor Emacs, Atom en VS Code, maar kan ook in batchmodus worden uitgevoerd vanaf de commandoregel.
Agda is gebaseerd op Zhaohui Luo's unified theory of dependent types (UTT), een typetheorie die lijkt op de Martin-Löf typetheorie.