MiniAgda: A toy dependently typed programming language with type-based termination.

MiniAgda is a tiny dependently-typed programming language in the style of Agda. It serves as a laboratory to test potential additions to the language and type system of Agda. MiniAgda's termination checker is a fusion of sized types and size-change termination and supports coinduction. Equality incorporates eta-expansion at record and singleton types. Function arguments can be declared as static; such arguments are discarded during equality checking and compilation. Recent features include bounded size quantification and destructor patterns for a more general handling of coinduction.

Downloads

• MiniAgda-0.2016.12.19.tar.gz [browse] (Cabal source package)
• Package description (as included in the package)

Maintainer's Corner

Package maintainers

• AndreasAbel

For package maintainers and hackage trustees

• edit package information

Candidates

• 0.2018.11.4, 0.2018.11.6, 0.2019.3.29, 0.2019.12.13, 0.2020.4.14, 0.2022.3.11, 0.2025.7.23