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

 Title: Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus Author: Michael Rawson (michaelrawson76 /at/ gmail /dot/ com) Submission date: 2017-07-09 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. BibTeX: @article{Name_Carrying_Type_Inference-AFP, author = {Michael Rawson}, title = {Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus}, journal = {Archive of Formal Proofs}, month = jul, year = 2017, note = {\url{http://isa-afp.org/entries/Name_Carrying_Type_Inference.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License