Agda

Total functional programming: termination, coverage, and the type universe hierarchy