Agda icon
Agda icon

Agda

Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs...

Cost / License

  • Free
  • Open Source

Application type

Platforms

  • Mac
  • Windows
  • Linux
Agda alternatives  
-
No reviews
2likes
0comments
4alternatives
0news articles

Features

Suggest and vote on features
No features, maybe you want to suggest one?

 Tags

  • proof-assistant
  • Math
  • proofs
  • formal
  • safety
  • verification

Agda News & Activities

Highlights All activities

Recent activities

Show all activities

Agda information

  • Developed by

    Unknown

  • Licensing

    Open Source and Free product.

  • Alternatives

    4 alternatives listed

  • Supported Languages

    • English

AlternativeTo Categories

Education & Reference, Development

Popular alternatives

View all
Agda was added to AlternativeTo by greenrd on and this page was last updated .
No comments or reviews, maybe you want to be first?
Post comment/review

What is Agda?

Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program.

Agda is a proof assistant. It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram, Matita and NuPRL.

Official Links