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] [Publish]

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

Versions 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.2020.4.14
Change log CHANGELOG
Dependencies array (>=0.3 && <0.6), base (>=4.6 && <5), containers (>=0.3 && <0.7), haskell-src-exts (==1.21.*), 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>
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 2020-04-14T11:38:19Z

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for MiniAgda-0.2020.4.14

[back to package description]

MiniAgda

Build Status Hackage

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 v1-update
  cabal v1-install alex
  cabal v1-install happy
  cabal v1-install MiniAgda

To build MiniAgda from source, replace the last command with

 make

Examples

See directories test/succeed/ and examples/.

Some examples are commented on the (dormant) MiniAgda blog.