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

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain]

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]

Properties

Versions0.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.2018.11.6
Change logCHANGELOG
Dependenciesarray (>=0.3 && <0.6), base (>=4.6 && <5), containers (>=0.3 && <0.6), haskell-src-exts (>=1.20 && <2.0), mtl (>=2.2.2 && <2.3), pretty (>=1.0 && <1.2) [details]
LicenseLicenseRef-OtherLicense
AuthorAndreas Abel and Karl Mehltretter
MaintainerAndreas Abel <andreas.abel@cse.gu.se>
CategoryDependent types
Home pagehttp://www.cse.chalmers.se/~abela/miniagda/
Bug trackerhttps://github.com/andreasabel/miniagda/issues
Source repositoryhead: git clone https://github.com/andreasabel/miniagda
Executablesminiagda
UploadedTue Nov 6 08:11:47 UTC 2018 by AndreasAbel

Downloads

Maintainers' corner

For package maintainers and hackage trustees


Readme for MiniAgda-0.2018.11.6

[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/