Preparing teaching material or tutorials

A great way to explore interesting topics in software science would be to prepare tutorials or lab packages for our courses. This will not only benefit yourself, but also introduce these important students to your fellow students. For example, our compiler course would greatly benefit some bonus material on advanced language engineering tools. You could write a simple tutorial about your topic of interest, but it would be more useful if you work it into a proper lab package with exercises and assessment guidelines and/or automated tests.

Creating an IDE for AKTk with Xtext or JetBrains MPS

AKTk is the language we use in our compilers course, during which you wrote a compiler, but a modern programming language obviously requires a great integrated development environment (IDE) with syntax highlighting and all that. As it happens, there are these things called language workbenches that make this really easy. There are two really prominent ones at the moment: Xtext and JetBrains MPS. You should select one and create a tutorial and demo (preferably in Estonian), so that we can use this in our compilers course. The main deliverable would be the demo code and documentation of your experience and potential pitfalls for using this in our courses.

Writing an Interpreter for AKTk in Truffle

During the compiler course, we wrote an interpreter for the AKTk language in a functional style. It would be nice to also demo an interpreter written in a more object-oriented style as a self-evaluating interpreter. In particular, you should try to implement the interpreter in the Truffle framework. Here, you should provide a little bit of background to the Truffle framework and describe and document your implementation.

Programming using Automata and Transducers

If you like finite automata, you should know that they are still alive and doing rather well in applications such as distributed string transformations. A great place to start learning about modern applications is Loris D'Antoni's Symbolic Automata page. He spent some time at Microsoft Research working with Margus Veanes on a number of domain-specific languages for string transformations. To begin with, you could choose one of these languages, such as bek, and explain what it can do and how it is implemented on top of symbolic automata. A toy implementation of a (subset) of the language in Java would also be interesting if you prefer programming over writing.

Types and Programming Languages

As a programmer, you have most likely ran into types before, but in our course, the type system was primitive. We would be interested in adding some opportunities for students to go a bit more deeply into type theory and possibly implement a type inference algorithm. This will require reworking the existing AKTk language and library to simplify these extensions.

Type theory is an interesting area of research as people are pushing the boundaries of what properties can be guaranteed by the type system. Some theoretical treatment of types would also be useful to learn and could be useful for our course. At the very extreme, one can view functional correctness properties as part of the types, which takes us to verified programming languages.

Testing so much that fear turned to boredom long ago? Try verified programming...

Verified programming is the future of programming. There are different approaches to this, such as Agda2, Coq, F*, but perhaps the easiest to get started with is Dafny. It has a simple tutorial on Rise4Fun and also runs in Visual Studio. It is thus very nice for learning this approach to programming, but it's not merely a toy: Dafny is used within the Ironclad/Ironfleet project at Microsoft Research to verify distributed systems.

Here, you could also write your own account of attempting to verify a small program. We will help you select a good example based on existing tutorials. Increasingly, we want program correctness to be a more important part of our courses, so it would be good to have introductions to many different approaches.

Amazon Web Services Uses Formal Methods (And So Can You!)

Since 2011, engineers at Amazon Web Services (AWS) have used formal specification and model checking to help solve difficult design problems in critical systems, why haven't you? Well, to begin with, you may want to find out How Amazon Web Services Uses Formal Methods.

The method they used was developed at Microsoft Research: TLA+ homepage. This is of course only one of many ways that designs can be validated. There are also different approaches and modelling languages, including Alloy and Promela. This topic could be approached in various ways. I would be interested in both basic overviews to popularize these methods here in Estonia as well as more in-depth descriptions of the tools and the theory behind it.

The Cybermen are Here: Excel's FlashFill and other threats of program synthesis

Have you wondered how Excel's Flash Fill feature works? This is an example of program synthesis, particularly Program by Example (PBE). There are many other choices in this area. Have a look at Summit Gulwani's page on program synthesis. You could write a very general overview of the field of program synthesis or focus on a single application and explain how it works. Program synthesis is a nice introduction to an emerging field that attempts to apply machine learning to program understanding and synthesis. For an overview of recent developments, see this blogpost and check out Microsoft's Deep Program Understanding project. Can the machines already program themselves?

Conjugate Hylo: The Mother of All Recursion Schemes

A "natural" transformation.

In Tartu's golden age of programming language research, before Jevgeni Kabanov went off founding ZeroTurnaround, he created a recursion scheme for dynamic programming, the dynamorphism. Almost ten years later, Oxford researchers have generalised this line of work, culminating in the Mother of All Recursion Schemes.

One of the classic papers in this field was written by Eric Meijjer, another start-up founder, and it may be worth starting your exploration of this topic with the classic paper Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. The point of some of this kind of work is explained in Ralf Hinze's Generics for the Masses. Learn about categorical programming, and maybe you might create the next big Estonian Start-Up... :)

Post-Rebel Dynamic Software Updates

The most successful commercial tool for dynamic reloading of Java classes is ZeroTurnaround's JRebel. Are there any academic developments in reloading since then? One very interesting tool seems to be Rubah. It would be very interesting to see what are the capabilities of this tool and compare it with JRebel. This is a good topic if you are also taking their course on Java Fundamentals and find Java technology interesting.