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{https://isa-afp.org/entries/Name_Carrying_Type_Inference.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.