Systems of polymorphic type assignment in LF
Robert W. Harper · KiltHub Repository · 2018
Abstract: "Several formulations of type assignment of the Damas-Milner language are studied, with a view toward their formalization in the logical framework LF, and the suitability of these encodings for direct execution by the logic programming language Elf."