Program Verification Made Easy with Imperative State Threads

This work formulates and implements a sublanguage for expressing verified, efficient, imperative programs inside a dependently typed functional programming language. The functional language base is Agda, and the new facilities are closely modeled on Haskell&rsquo;s <code>ST</code>. I place emphasis on minimizing the complexity of the design and leveraging Agda&rsquo;s complex type system to provide the most intuitive experience possible. I also develop a principled proof automation macro, which is robust and should be extensible to new data types. I demonstrate the capability of my system by implementing well-known imperative algorithms such as the loop-based calculation of the Fibonacci numbers and insertion sort.