You could have invented normalization-by-evaluation — August 9, 2025
If you’re implementing some sort of dependently typed language, you’ve probably heard of normalization-by-evaluation, or NbE. Wikipedia describes NbE like this:
Read more
I’m a CS undergrad at Yale, primarily interested in programming languages and knowledge management. You can find me on Github and LinkedIn. My email is <first>.<last>@<school>.edu
If you’re implementing some sort of dependently typed language, you’ve probably heard of normalization-by-evaluation, or NbE. Wikipedia describes NbE like this:
Read moreA while back I got interested in quantifier elimination in FOL, which led me to the extremely interesting $\epsilon$-calculi! For those not familiar with Hilbert’s $\epsilon$ operator, it is a term-forming operator satisfying the following axiom.
Read more