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]
Downloads
- MiniAgda-0.2018.11.4.tar.gz [browse] (Cabal source package)
- Package description (revised from the package)
Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.
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 |
|---|---|
| Change log | CHANGELOG |
| Dependencies | array (>=0.3 && <0.6), base (>=4.6 && <5), containers (>=0.3 && <0.6), haskell-src-exts (>=1.20 && <1.21), mtl (>=2.2.2 && <2.3), pretty (>=1.0 && <1.2) [details] |
| Tested with | ghc ==7.6.3, ghc ==7.8.4, ghc ==7.10.3, ghc ==8.0.2, ghc ==8.2.2, ghc ==8.4.4 |
| License | LicenseRef-OtherLicense |
| Author | Andreas Abel and Karl Mehltretter |
| Maintainer | Andreas Abel <andreas.abel@cse.gu.se> |
| Revised | Revision 1 made by AndreasAbel at 2019-03-29T22:58:37Z |
| 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 2018-11-04T09:58:13Z |
| Distributions | |
| Reverse Dependencies | 1 direct, 0 indirect [details] |
| Executables | miniagda |
| Downloads | 7303 total (35 in the last 30 days) |
| Rating | 2.0 (votes: 1) [estimated by Bayesian average] |
| Your Rating | |
| Status | Docs not available [build log] Last success reported on 2018-11-04 [all 2 reports] |