Abstract: 
I formalise a Churchstyle simplytyped
\(\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. 
BibTeX: 
@article{Name_Carrying_Type_InferenceAFP,
author = {Michael Rawson},
title = {Verified Metatheory and Type Inference for a NameCarrying SimplyTyped Lambda Calculus},
journal = {Archive of Formal Proofs},
month = jul,
year = 2017,
note = {\url{http://isaafp.org/entries/Name_Carrying_Type_Inference.html},
Formal proof development},
ISSN = {2150914x},
}
