[isabelle] new AFP entry: Name_Carrying_Type_Inference


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

 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 [0].

[0]: http://www.openthesis.org/documents/Verified-Metatheory-Type-Inference-Simply-603182.html


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.