PL Glossary

This page is a compiled list of terms in PL that I’ve had to work to understand.

Elaborator: A function/program that maps a surface syntax into a core syntax. Usually this involves desugaring and adding more annotations, hence the name.
Intrinsically scoped: A method of representing your object syntax in a way that enforces its scoping rules in the type system of your metalanguage.
Intrinsically scoped: A method of representing your object syntax in a way that enforces its typing rules in the type system of your metalanguage. Works for smaller calculi, but extending this to dependent types is currently an open problem.
Spine: A more efficient representation of function application with multiple arguments over the usual left-associative application operator. ¹

Judgemental Equality: The same thing as definitional equality. Judgemental equality holds for two things when they have exactly the same semantically (equal by definition).²

(Capture-Avoiding) Substitution: Given Γ, x : A ⊢ b : B and Γ ⊢ a : A then Γ ⊢ b[a/x] : B. Effectively, substitutions allow us to shorten a context. cf. weakening.³
Substitution Calculus: While the usual substitution operator [a/x] is defined on single terms, we can consider arbitrary compositions of substitutions and weakenings as morphisms between contexts. This presentation gives rise to a substitution calculus. We denote ρ : Γ → Δ as Γ ⊢ ρ : Δ, sending elements of Δ to Γ. Usually we drop variable names when working in the substitution calculus. ⁴
Weakening: Given Γ ⊢ b : B and Γ ⊢ A type, then Γ, x : A ⊢ b : B. Effectively, weakenings allow us to extend a context. cf. substition.⁵