Andreas Abel: MiniAgda: Termination Checking using Sized Types
MiniAgda: Checking Termination using Sized Types
MiniAgda is a small functional programming language with dependent
types in which all programs terminate. Originally implemented by Karl
Mehltretter for his diploma thesis in 2007, I have added many new
features over the last 2 years.
In MiniAgda one can define data types such as lists and trees, but
also so called "codata" types for infinite structures such as streams.
Sizes can attached to these types in a uniform way, denoting upper
bounds for the tree height in case of data, and a lower bound on the
depth for codata. Sizes are used to aid the termination checker,
which handles mutual recursion and indirect descent through another
function. One of the new features is a constraint solver for sizes.
In the talk, I will present MiniAgda by some example programs, and
explain the principles behind termination checking with sizes and the
algorithm for solving the constraints.
abgelegt unter: Oberseminar