Title: Theory / Unimportant / CS / Fundamental / Practical Foundations for Programming Language{ / 2 Statics and Dynamics=

Name: A typing context
Definition: A map associating to some variable their type
Chapter: 4
Section: 2
Denoted by: \(\Gamma\)

Name: \(x\) is of type \(\tau\)
Chapter: 4
Section: 2
Variables: \(x\) a variable,
\(\tau\) a type
Notation: \(x:\tau\)

Definition: Assuming that for each \(i\), with context \(\Gamma\), and extra variables \(x_{i,j}\) of type \(\tau_{i,j}\), \(e_i\) has type \(\tau_i\), it follows that \(e\) has type \(\tau\)
Chapter: 4
Section: 2
Notation: \(\frac{(\Gamma,x_{i,1}:\tau_{i,1},\dots,x_{i,n_i}:\tau_{i,n_i}\vdash e_i:\tau_i)_i}{\Gamma\vdash e:\tau}\)

Smaller0: \(\Gamma,x:\tau\vdash e':\tau'\)
Greater0: \(\Gamma\vdash [e/x]e':\tau'\)
Chapter: 4
Section: 2
Index: 4, 5
Kind: Lem
Smaller to greater: iff
Assuming: \(\Gamma\vdash e:\tau\)

Question: The construct of a languages are classified into
Answer: the introduction
Chapter: 4
Section: 3
Answer3: the elimination
Extra: Go chapter 5