We are working towards making Kotlin a safer language.  One approach we are looking into is uniqueness typing, where some references are statically checked to not be aliased by any other reference.  We have a type system outlined, and are currently implementing it in a plugin.  In this project, we are looking for an intern who can formalise our system and prove that it provides the guarantees we expect.

Your work will consist of modelling a subset of Kotlin in the Lean proof assistant and then stating and proving theorems about it.  This may require adapting our idea or coming up with something new.  We are also looking into further extending the system, for example by adding support for path-dependent types or lifetime constraints.

For more details about the system, check out the master thesis in which a former JetBrains intern developed this idea: https://thesis.unipd.it/handle/20.500.12608/70919

• Currently pursuing or recently graduated from a Computer Science or Mathematics degree, or a degree in a related field.

• Excellent command of oral and written English

• Familiarity with programming language semantics

• Experience with proof assistants, especially Lean, is a plus