Email Gateway (Aug 22 2022 at 15:46): Email Gateway (Aug 22 2022 at 15:46):From: Gerwin Klein <gerwin.klein@data61.csiro.au>
https://www.isa-afp.org/entries/Name_Carrying_Type_Inference.shtml
Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus
by Michael Rawson
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 [0].
[0]: http://www.openthesis.org/documents/Verified-Metatheory-Type-Inference-Simply-603182.html
Enjoy!
Gerwin
Last updated: Apr 25 2024 at 12:23 UTC