Unraveling recursion: compiling an IR with recursion to System F

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.