Abstract: “We investigate compilation and verification techniques for functional language compilers by developing and verifying a toy optimizing compiler from the untyped lambda calculus to Brainfuck. Our key optimization is provisional type inference, in which the compiler guesses the latent type of a lambda calculus subterm and produces optimized Brainfuck code for that subterm, falling back on the naive slow path code in contexts where that guess is incorrect. Provisional type inference allows the compiler to be extended with additional optimized Brainfuck implementation of common idioms and data structures with minimal additional verification burden.”