IOHK | Paper

Library > System F in Agda, for fun and profit

System F in Agda, for fun and profit

October/2019, MPC'19


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].