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

[ dependent-types, mit, program ] [ Propose Tags ] [ Report a vulnerability ]

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

Maintainer's Corner

Package maintainers

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
Dependencies array (>=0.3 && <0.6), base (>=4.2 && <4.8), containers (>=0.3 && <0.6), haskell-src-exts (>=1.14 && <1.15), IfElse (>=0.85 && <2.0), mtl (>=2.0 && <2.1 || >=2.1.1 && <2.2), pretty (>=1.0 && <1.2) [details]
Tested with ghc ==7.6.3, ghc ==7.8.2
License LicenseRef-OtherLicense
Author Andreas Abel and Karl Mehltretter
Maintainer Andreas Abel <andreas.abel@ifi.lmu.de>
Category Dependent types
Home page http://www.tcs.ifi.lmu.de/~abel/miniagda/
Bug tracker http://hub.darcs.net/abel/miniagda/issues
Source repo head: darcs get http://hub.darcs.net/abel/miniagda
Uploaded by AndreasAbel at 2014-05-05T14:09:31Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Executables miniagda
Downloads 7311 total (21 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 2015-05-22 [all 8 reports]