The current memory model makes heavy use of memoization. Implementing a more efficient reduction algorithm along with this would make our evaluation machine much more efficient. One may take inspiration from this project, which implements NBE with no memoization in rust: https://github.com/brendanzab/rust-nbe-for-mltt. This would also allow us to have two different reduction processes in our kernel, which would allow us to "verify" our current implementation, both in terms of correctness and performance.