Lambda calculi are often used as intermediate representations for compilers. However, they require extensions to handle higherlevel features of programming languages. In this paper we show how to construct an IR based on System Fμω which supports recursive functions and datatypes, and describe how to compile it to System Fμω. Our IR was developed for commercial use at the IOHK company, where it is used as part of a compilation pipeline for smart contracts running on a blockchain.
# Available in: pdf, doi.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.
# Available in: pdf, doi.