Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus

Michael Rawson 📧

July 9, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Name_Carrying_Type_Inference