Agda icon
Agda icon

Agda

 2 likes

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...

License model

  • Free • Open Source

Application type

Platforms

  • Mac
  • Windows
  • Linux
Agda alternatives  
  No rating
2likes
0comments
3alternatives
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

No activities found.

Agda information

  • Developed by

    Unknown

  • Licensing

    Open Source and Free product.

  • Alternatives

    3 alternatives listed

  • Supported Languages

    • English

AlternativeTo Categories

Education & Reference, Development

Popular alternatives

View all

Our users have written 0 comments and reviews about Agda, and it has gotten 2 likes

Agda was added to AlternativeTo by greenrd on Aug 20, 2010 and this page was last updated Nov 27, 2014.
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