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

[ dependent-types, 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]
Versions [faq] 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
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:40:14Z
Distributions NixOS:0.2020.4.14
Executables miniagda
Downloads 5628 total (3 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs not available [build log]
Last success reported on 2020-04-14 [all 2 reports]

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.