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:

Dependent types for programmers — August 9, 2025

I’ll use tagged unions to introduce dependent types. Here’s a tagged union int_or_char.

enum int_or_char_tag {
    INT_TAG,
    CHAR_TAG
}
union int_or_char_data {
    int int_data;
    char char_data
}
struct int_or_char {
    enum int_or_char_tag tag;
    union int_or_char_data data;
}

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.