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.
[Skip to Readme]
Modules
[Index] [Quick Jump]
Downloads
- MiniAgda-0.2025.7.23.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
Versions [RSS] | 0.2014.1.9, 0.2014.5.5, 0.2014.9.12, 0.2016.12.19, 0.2017.2.18, 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 |
---|---|
Change log | CHANGELOG |
Dependencies | array (>=0.3 && <0.6), base (>=4.9 && <5), containers (>=0.3 && <1), haskell-src-exts (>=1.21 && <1.22), MiniAgda, mtl (>=2.2.1 && <2.4), optparse-applicative (>=0.16.0.0 && <1), pretty (>=1.0 && <1.2), string-qq, transformers [details] |
Tested with | ghc ==9.12.2, ghc ==9.10.2, ghc ==9.8.4, ghc ==9.6.7, ghc ==9.4.8, ghc ==9.2.8, ghc ==9.0.2, ghc ==8.10.7, ghc ==8.8.4, ghc ==8.6.5, ghc ==8.4.4, ghc ==8.2.2, ghc ==8.0.2 |
License | MIT |
Author | Andreas Abel and Karl Mehltretter |
Maintainer | Andreas Abel <andreas.abel@cse.gu.se> |
Category | Dependent types |
Home page | http://www.cse.chalmers.se/~abela/miniagda/ |
Bug tracker | https://github.com/andreasabel/miniagda/issues |
Source repo | head: git clone https://github.com/andreasabel/miniagda |
Uploaded | by AndreasAbel at 2025-07-23T12:49:00Z |
Distributions | |
Reverse Dependencies | 1 direct, 0 indirect [details] |
Executables | miniagda |
Downloads | 7451 total (16 in the last 30 days) |
Rating | 2.0 (votes: 1) [estimated by Bayesian average] |
Your Rating | |
Status | Docs available [build log] Last success reported on 2025-07-23 [all 1 reports] |