Abstract
I formalise a Church-style simply-typed
\(\lambda\)-calculus, extended with pairs, a unit value, and
projection functions, and show some metatheory of the calculus, such
as the subject reduction property. Particular attention is paid to the
treatment of names in the calculus. A nominal style of binding is
used, but I use a manual approach over Nominal Isabelle in order to
extract an executable type inference algorithm. More information can
be found in my undergraduate
dissertation.