Programming Languages & Functional/Verified programming

If you like programming and would like to improve your craft, there is no better way than exploring programming language design and implementation.

Implementing your own programming language

You can build your own toy language to deepen your knowledge of programming and then start experimenting with exciting new programming language features. We are more interested in the implementation of functional languages and lazy evaluation, but this is your language and you can decide yourself. Here are a few directions that you could consider exploring:

  • Extending the type system to reason about programs (dependent types, liquid types).
  • Experiment with novel ideas to manage effect and impurity (see the Eff language).
  • Design the language with abilities to verify correctness under weak memory consistency.
  • Focusing on a specific domain. For quantum programming, however, turn to Ketita Labs.

Adding language and tooling support to IntelliJ IDEA

The development environment is just as important for the programming experience as the programming language. It would be a great contribution to add support for programming languages and tools to the IntelliJ IDEA. Here are some examples:

  1. I quite like the KeY project, except all their tools are using Eclipse, which I do not like. If you are interested in IntelliJ platform technology and would like to make a nice contribution to an open source project, creating IntelliJ Plug-ins for these KeY tools would be a great idea. Initially, all we need is support for OpenJML to IntelliJ IDEA.
  2. Contracts for Java, Cofoja, is a more lightweight verification framework than JML or KeY. It simply allows one to write pre- and post-conditions as Java annotations. These are checked at runtime. This is very much like OpenJML, but the use of annotations means that it can be implemented as a Java library and this is more modern. The small problem here, though, is that annotations aren't syntactically checked by the IDE and are only displayed as plain strings. It would be awesome to have the typical IDE support for assertions written in these annotations.
  3. Your own ideas ...

Real-World Functional Programming

Varmo Vene always offered students the opportunity to do anything they want for their thesis... as long as they did this in Haskell. This offer still stands, although we recommend the truly brave to try verified programming!

You are welcome to program anything you want, just anything, as long as it is done in an elegant functional language and you really apply novel techniques to manage shared state. You should be able to convince (at least yourself) that this approach results in a more reliable system than the imperative style. At the moment, there is a lot of buzz around web development with ReasonML or Elm. If you want to build a prototype web app, you can combine this with learning new approaches and programming techniques.