Theoretical Topics in Programming Languages

"There is nothing more practical than a useful theory", and there is nothing more useful than programming language theory. Here are some exciting topics in programming language research:

Assigning meanings to programs

Do you believe programs have meanings? If not, you should perhaps rather do Software Engineering, but if you agree that programs are not arbitrary token sequences and are interested in figuring out what these programs actually mean, you are in the right place!

Semantics is the mathematical discipline that gives meanings to programs. Härmel Nestra has explored an interested topic in this field: non-standard semantics. These are deviant semantics that are suitable for particular uses, such as program slicing. For more information, see non-standard semantics.

Types and Programming Languages

As a programmer, you have most likely ran into types in some form or another. Type theory is an interesting area of research as people are pushing the boundaries of what properties can be guaranteed by the type system. At the very extreme, one can view functional correctness properties as part of the types and we arrived at proof assistance and dependently typed languages.

The practical side of type systems is also worth exploring, such as the comparison of ML modules and Haskell type classes. To what extent can Haskell type classes express the same as the powerful module system of ML? More info: ML moodulprogrammeerimise ja Haskelli tüübiklasside võrdlus (in Estonian).

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.

As part of a joint project with a company that helps publishers create e-books, we are interested in looking at how the Program-by-Example paradigm could be applied to improve the process of generating epub documents from pdf inputs.

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... :)

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.