I think I will keep some research notes online. I've tried installing MathJax, so this should not be too unreadable, either. Let me begin with the typing of the simply typed lambda calculus, as is traditional.
\[
\begin{array}{lcl}
A & ::= & 1 \bnfalt A \times B \bnfalt A \to B \\
e & ::= & () \bnfalt (e,e) \bnfalt \fst{e} \bnfalt \snd{e} \\
& | & x \bnfalt e\;e' \bnfalt \fun{x:A}{e}
\end{array}
\]
\[
\begin{array}{ll}
\rule{x:A \in \Gamma}
{\judge{\Gamma}{x}{A}} &
\rule{ }
{\judge{\Gamma}{()}{1}}
\\
& \\
\rule{\judge{\Gamma,x:A}{e}{B}}
{\judge{\Gamma}{\fun{x:A}{e}}{A \to B}} &
\rule{\judge{\Gamma}{e}{A \to B} & \judge{\Gamma}{e'}{A}}
{\judge{\Gamma}{e\;e'}{B}}
\\
& \\
\rule{\judge{\Gamma}{e}{A} & \judge{\Gamma}{e'}{B}}
{\judge{\Gamma}{(e,e')}{A \times B}}
\\
& \\
\rule{\judge{\Gamma}{e}{A \times B}}
{\judge{\Gamma}{\fst{e}}{A}} &
\rule{\judge{\Gamma}{e}{A \times B}}
{\judge{\Gamma}{\snd{e}}{B}}
\end{array}
\]
