Agda

Niet te verwarren met Ada (programmeertaal).

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
Portaal    Informatica

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.

1. ↑ Release 2.7.0.1 (12 september 2024). Geraadpleegd op 20 september 2024.