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: Difference between revisions
From WG 2.11
Jump to navigationJump to search
Created page with " == "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..." |
(No difference)
|
Latest revision as of 11:10, 3 October 2024
"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.
