Haskell and Agda code for the article "Calculating Compilers Effectively"

The Haskell and Agda source code for the paper Calculating Effectful Compilers Haskell (print.hs, state.hs, non-det.hs) In these files we give practical implementations of each of the three effects we consider in the paper. For each one, we include the full source code as described in the paper itself, and full definitions for each of the concrete effect interpretations. Agda (print.agda, state.agda, non-det.agda, lemmas.agda) As noted in the paper, we use Agda to formally verify the correctness of our calculations. These four files constitute those proofs. We use function extensionality, which is postulated in lemmas.agda. Each Agda file begins by translating the types and functions from Haskell into Agda's syntax. We prove all relevant results: * The functor and monad laws for each effect type * Compiler correctness exec (comp e c) s = do v