Agda-curious? An Exploration of Programming with Dependent Types
I explore programming with the dependently typed functional language, AGDA. I present the progress which AGDA has made, demonstrate its usage in a small development, reflect critically on the state of the art, and speculate about the way ahead. I do not seek to persuade you to adopt AGDA as your primary tool for systems development, but argue that AGDA stimulates new useful ways to think about programming problems and deserves not just curiosity but interest, support and contribution.
dependent types languages design theory