Hackage :: [Package]

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

[ dependent-types, mit, program ] [ Propose Tags ]

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

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

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
Change log CHANGELOG
Dependencies array (>=0.3 && <0.6), base (>=4.6 && <5), containers (>=0.3 && <0.7), haskell-src-exts (>=1.21 && <1.22), mtl (>=2.2.2 && <2.3), pretty (>=1.0 && <1.2) [details]
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-30T12:09:12Z
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 2019-03-29T13:40:58Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Executables miniagda
Downloads 7027 total (0 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 2019-03-29 [all 2 reports]

Readme for MiniAgda-0.2019.3.29

[back to package description]

MiniAgda

A prototypical dependently typed languages with sized types and variances.

Installation

Requires GHC and cabal, for instance via the Haskell Platform. In a shell, type

  cabal update
  cabal install alex
  cabal install happy
  cabal install MiniAgda

Examples

See test/succeed/ and examples/