The latest version of MiniAgda is 0.2022.3.11-0.

MiniAgda

Version 0.2017.2.18 revision 1 uploaded by HerbertValerioRiedel.

Package meta

Synopsis
A toy dependently typed programming language with type-based termination.
Description

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.

Author
Andreas Abel and Karl Mehltretter
Bug reports
https://github.com/andreasabel/miniagda/issues
Category
Dependent types
Copyright
n/a
Homepage
http://www.tcs.ifi.lmu.de/~abel/miniagda/
Maintainer
Andreas Abel <andreas.abel@ifi.lmu.de>
Package URL
n/a
Stability
n/a

Components