System F in Agda, for fun and profit

System F, also known as the polymorphic λ-calculus, is a typed λ-calculus independently discovered by the logician Jean-Yves Girard and the computer scientist John Reynolds. We consider F_ωµ, which adds higher-order kinds and iso-recursive types. We present the first complete, intrinsically typed, executable, formalisation of System F_ωµ that we are aware of. The work is motivated by verifying the core language of a smart contract system based on System F_ωµ. The paper is a literate Agda script [14].