Type-Safe Programming with Versions

Most of existing programming languages treat versions of program modules outside of the language semantics. Programs are written, type-checked, and compiled with respect to modules in specific versions, yet later linked together in possibly different versions, which caused problems of conflicts and inconsistencies. This project aim at designing a programming language that treats versions inside of the language semantics. By conceptually adding versions to every value in a running program, the language enables to use different versions of a module at the same time in a type-safe fashion.

The project will investigate a core calculus called λVL, the design and the implementation of an OOP language with versions called BatakJava, and case studies of software development with versions.