Content deleted Content added
→Agda (programming language): Added links Tags: canned edit summary Mobile edit Mobile app edit Android app edit |
m linking |
||
Line 107:
=== Termination checking ===
Agda is a [[Total functional programming|total language]], i.e., each program in it must terminate and all possible patterns must be matched. Without this feature, the logic behind the language becomes inconsistent, and it becomes possible to prove arbitrary statements. For [[termination checking]], Agda uses the approach of the Foetus termination checker.<ref>Abel, Andreas. "foetus – Termination checker for simple functional programs." ''Programming Lab Report'' 474 (1998).
[http://www.tcs.informatik.uni-muenchen.de/~abel/foetus.pdf]
| |||