Agda (programming language): Difference between revisions

Revision as of 23:04, 28 February 2020

Revision as of 20:05, 29 February 2020

Line 1:

{{short description|Functional programming language}}

{{Infobox programming language

| name = Agda

| logo = Agda's official logo.svg

| logo alt = A stylized chicken in black lines and dots, to the left of the name “Agda” in sans-serif test with the first letter slanted to the right.

| paradigm = [[functional programming|Functional]]

| year = {{Start date and age|2007}}, (1.0 in {{Start date and age|1999}})

| designer = Ulf Norell; Catarina Coquand (1.0)

| developer designer = Ulf Norell; Catarina Coquand (1.0)

| designer developer = Ulf Norell; Catarina Coquand (1.0)

| written in = Haskell

| latest release version = 2.6.0.1

| latest release date = {{Start date and age|2019|05|17}}

| latest test version =

| latest test date = =

| typing = [[Strong typing|strong]], [[Static typing|static]], [[Dependent typing|dependent]], [[Nominal typing|nominal]], [[Manifest typing|manifest]], [[Inferred typing|inferred]]

| implementations = =

| dialects = =

| influenced = [[Idris (programming language)|Idris]]

| influenced by programming language = [[Coq]], [[Epigram (programming language)|Epigram]], [[Haskell (programming language)|Haskell]]

| influenced by = [[Coq]], [[Epigram (programming language)|Epigram]], [[Haskell (programming language)|Haskell]]

| license = [[BSD licenses|BSD-like]]<ref>[http://code.haskell.org/Agda/LICENSE Agda license file]</ref>

| file ext = <code>.agda</code>, <code>.lagda</code>, <code>.lagda.md</code>, <code>.lagda.rst</code>, <code>.lagda.tex</code>

| operating system = [[Cross-platform]]

| website = {{URL|wiki.portal.chalmers.se/agda}}

}}

'''Agda''' is a [[Dependent type|dependently typed]] [[functional programming]] language originally developed by Ulf Norell at [[Chalmers University of Technology]] with implementation described in his PhD thesis.<ref>Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007. [http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf]