Elektrine lite

← Feed

Zhixuan Yang

zyang@mathstodon.xyz

<p>interested in algebraic and logical methods in computer science, Lecturer at the University of Exeter</p>

Posts

  • View post

    https://yangzhixuan.github.io/NbE.html My (rather long) blog post on normalisation by evaluation is online now. In this post I show how we can optimise a naive substitution-based applicative-order normaliser of untyped calculus step by step, leading us to reconstruct NbE as &amp;quot;weak-applicative-order normalisation with meta-level laziness, lazy substitution, and de Bruijn levels&amp;quot;. We will also examine some &amp;quot;adversarial exploit&amp;quot; that makes NbE slow and use the in...