[Agda] origin of "Agda"?

[Andreas Abel]

Unfortunately, the account given by Vilhelm is correct, although we try 
to keep this embarrassing part of history under the carpet... :D

Certainly a pun / antithesis to Coq.

On 06.07.2016 21:51, Vilhelm Sjoberg wrote:
> Agda is a female given name in Swedish. I've heard claims that the name
> of the computer language is a reference to the humorous song "Hönan
> Agda" [Agda the hen] by Cornelis Vreeswijk. A companion for Coq, as it were.
>
> Vilhelm
>
> On Wed, Jul 6, 2016 at 3:03 PM, Peter Selinger <selinger at mathstat.dal.ca
> <mailto:selinger at mathstat.dal.ca>> wrote:
>
>     Does anyone know why Agda is called Agda? I realize the name is based
>     on the 1999 "Agda 1" by Catarina Coquand, but what was the meaning of
>     the original name? Is it an acronym (I noticed that some of the early
>     papers spell it AGDA)? Or is it someone's name? I looked at some of
>     the Agda 1 materials, but found no explanation.
>
>     Just curious, -- Peter
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://urldefense.proofpoint.com/v2/url?u=https-3A__lists.chalmers.se_mailman_listinfo_agda&d=CwICAg&c=-dg2m7zWuuDZ0MUcV7Sdqw&r=9KjgxQ7ApO6qc9JMInnxwZoTtVeCJRKTHVqtyQ8B26o&m=_5fNF7bf-eyi6zA9jWMMfBBIxrn8h6szFfjA0bOokTE&s=NDYrwURXbfhU7uJYrOJSveUmPZbbx0FlJC4eendsqoc&e=
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/