---
key: pl/agda
kind: plang
name: "Agda"
url: https://plangs.page/agda
---

# Agda

> Dependently typed functional programming language and proof assistant used for writing and verifying proofs.

Dependently typed functional programming language and proof assistant, originally developed at Chalmers University of Technology. It is used for writing and verifying proofs using a functional style, and it uniquely integrates programming and proving without a separate tactic language. Agda employs rich type systems such as dependent types, supporting inductive families and parameterized modules.

## Facts

- Appeared: 2007
- Homepage: https://wiki.portal.chalmers.se/agda/pmwiki.php
- GitHub: https://github.com/agda/agda
- Languish ranking: #217

## Relationships

### Paradigms

- [Functional](https://plangs.page/paradigm/functional)
- [General-Purpose](https://plangs.page/paradigm/general-purpose)

### Platforms

- [Cross-Platform](https://plangs.page/platform/cross)

### Type Systems

- [Dependent](https://plangs.page/type-system/dependent)
- [Inferred](https://plangs.page/type-system/inferred)
- [Manifest](https://plangs.page/type-system/manifest)
- [Nominal](https://plangs.page/type-system/nominal)
- [Static](https://plangs.page/type-system/static)
- [Strong](https://plangs.page/type-system/strong)

### Influenced By

- [Coq](https://plangs.page/coq)
- [Haskell](https://plangs.page/haskell)

### Influenced

- [Idris](https://plangs.page/idris)

### Written With

- [Haskell](https://plangs.page/haskell)

### Licenses

- [BSD](https://plangs.page/license/bsd)

### Tags

- [Automation](https://plangs.page/tag/automation)
- [Compiler](https://plangs.page/tag/compiler)
- [Control](https://plangs.page/tag/control)
- [Industrial Control](https://plangs.page/tag/industrial)
- [Interpreter](https://plangs.page/tag/interpreters)
- [Proof Assistant](https://plangs.page/tag/proofs)