Gradual Typing: Isabelle/Isar Formalization
Siek, Jeremy; Taha, Walid
DateApril 7, 2006
This report formalizes a gradual type system using the Isabelle/Isar proof language and proof assistant. Gradual typing combines static typing and dynamic typing in the same language, allowing a programmer to gradual migrate portions of a program between the two typing disciplines.