Stuck in a (While) Loop
Assessing Coinduction in Agda using Cyclic Program Traces
C.C. Stokka (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Bohdan Liesnikov – Mentor (TU Delft - Programming Languages)
J.G.H. Cockx – Mentor (TU Delft - Programming Languages)
Diomidis Spinellis – Graduation committee member (TU Delft - Software Engineering)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Interactive proof assistants such as Agda have powerful applications in proving the correctness of software. Non-terminating programs, such as those containing infinite loops, result in execution paths of infinite length, which can introduce challenges when reasoning about such programs. Agda, as a total language, relies on the concept of coinduction for reasoning about potentially infinite structures. Mutiple methods for coinduction exist in Agda, each with difficulties related to usage or soundness. To evaluate these limitations, I implement traces and semantics for a simple imperative programming language, While, using Agda's various methods of coinduction. The different encodings are compared in their abilities and limitations, and from this I identify areas for improvement in Agda's coinduction support.