Milestones
The project is to be completed incrementally, with the following milestones as our guide. The project begins with a literature review of the papers and related work to understand the theoretical foundations of the type inference algorithms. The team would also be writing the implementations of the type inference algorithms while performing the literature review. This would involve understanding the algorithms and translating them into code. The team plans on completing this by the end of the first month. The first major milestone would then be to model a complete type-checker for the STLC without type annotations, supported with a REPL, parser and pretty-printer for (algorithmic) derivations. From there, it will be important to identify the subset of rules that are relevant to the STLC and implement them in the chosen language. This will involve implementing the type inference algorithm, the REPL, parser, and pretty-printer for the STLC, as well as adapting the syntax from the papers accordingly. This would be mostly complete by the end of November. Once the STLC and supporting tools have been implemented, our team will proceed to implement other features based that are a natural step forward from the STLC. This may include rethinking the implementations to possibly uncover some sort of a monadic structure, or have the algorithm return the inferred types, or even elaborate the STLC to a target calculus. These could be accomplished by the end of December or the start of January.