On Friday October 17, this site was moved to a new server, https://mw.hh.se. The original address will continue to work. Whithin a week or two this site will return to the original address. /Peo HH IT-dep
WG211/M24Brady
From WG 2.11
"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.
