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.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License