WG211/M24Brady

"Normalisation by Compilation": Typechecking Dependent Types via the Scheme Runtime

I will describe the progress on a new implementation of the Idris core, which aims to improve evaluator performance during type checking by compiling open terms to Scheme, and using the Chez Scheme runtime to evaluate those terms. I will explain the challenges, particularly the challenge of representing free variables in the runtime, and show how to incorporate it into the type checking and unification algorithms.