Abstract. This pearl examines how to verify functional programs written using the state monad. It uses Coq’s Program framework to provide strong specifications for the standard ...
We present four coinductive operational semantics for the While language accounting for both terminating and non-terminating program runs: big-step and small-step relational semant...
Abstract. We give an overview of Agda, the latest in a series of dependently typed programming languages developed in Gothenburg. Agda is based on Martin-L¨of’s intuitionistic t...
Abstract. We present a Coq formalization of constructive ω-cpos (extending earlier work by Paulin-Mohring) up to and including the inverselimit construction of solutions to mixed-...