Eashan Hatti

\[\frac{ \Gamma, x : A \vdash e : B }{ \Gamma \vdash \lambda x. e : \Pi_{x : A} B }\]

I’m a CS undergrad at Yale, primarily interested in programming languages and proof assistants. You can find me on Github and LinkedIn.

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:

Fun with $\epsilon$-calculi — August 7, 2025

A 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.