For Uppsala/Prospective Students
My main research interest is design and implementation of programming languages and the connection between programming languages and software engineering.
With respect to programming languages, I am interested in programming abstractions — ways to express and model properties of interest in programs, and how to fortify abstractions and how to capture and enforce programmer intent. Abstraction is an essential task of programming and involves hiding details and emphasising rules and "interfaces". For example, a stack is an abstraction that presents a certain interface: elements are inserted and removed from the same end, and the only way to manipulate the order of elements on a stack are by popping them and pushing them back in a different order. The stack concept abstracts from the concrete implementation and emphasises the rules by which a stack can be manipulated to maintain its "stack-ness". A classic text book-example of a stack implementation is through a set of linked nodes, each holding an element. Unless the implementation of the stack abstraction is properly fortified, it could for example be possible for a user of a stack to gain access to its stack nodes and through direct manipulation of the stack nodes reorder elements or delete elements, or replace them, etc. — clear violations of "stack-ness".
A properly fortified abstraction is possible to replace by another — for example a stack implemented as an array. The ability to swap entire building blocks of a program for others is important because it allows us to alter non-functional aspects of a program (a classic example of a non-functional aspect is performance, another is security). This example also illustrates a connection with software engineering.
Related is the capturing and enforcing of programmer intent — programming languages typically focus on helping programmers perform calculations but do not understand non-functional aspects of the system, and are therefore unable to help programmers write code that correspond to their intentions. Mistakes and misconceptions surface in testing (if the tests are good enough, of course), where they may show up as errors whose root causes are hard to determine. A classic example is thread safety — the ability to use share something between threads that concurrently access it. Determining whether a piece of code is thread-safe can be very hard, and require lots of so-called non-local reasoning, i.e., checking many other places of the code that may somehow interplay with the code of interest.
Going back to the stack example before — whether it is safe to share a stack abstraction across threads either requires knowledge of its concrete implementation (e.g., we know it uses some internal form of synchronisation), or access to documentation. Proper abstraction dictates that we should not rely on one specific implementation (for software engineering reasons, for example so that we can swap one stack implementation for for another). Documentation however can be wrong, for example because the programmer thinks something is thread-safe that really isn't. This can happen for many reasons. For example, imagine the stack relies on some library L in its implementation. When the programmer implemented the stack, she checked the functions in L for thread-safety, but since then, L has changed and some functions are no longer thread-safe. Because most programming languages lack the ability to talk about thread-safety (as it is a non-functional property of the code) the compiler cannot warn us about this important change and consequently, the documentation of the stack incorrectly states it is thread-safe.
Enabling the programmer to state her intent about thread-safety allows the compiler to check that the implementation of the stack is thread-safe, and also captures the error of the changing properties of some functions in library L when the stack is recompiled against the updated L library.
Static checking (i.e., at compile-time) is conservative by nature, meaning that some programs will be incorrectly rejected (or raise warnings) because the compiler is unable to prove that they satisfy the intended properties. This is unfortunate, but I believe that a small number of false positives is a small price to pay for machine-checked proofs of fulfilment of relevant properties of source code. If something is labelled thread-safe, we should be able to rely on it.
This brings me to programming languages implementation. If compilers become powerful enough to guarantee certain properties of interest of a program, it is possible to compile and/or execute these programs more efficiently. For example, if I know that some object O is only visible through this one pointer, I can temporarily copy O into CPU registers and make lots of updates on O without slow and costly updates of main memory so that a possible (however unlikely) concurrent reader of O is guaranteed to see a up-to-date value. Similar arguments can be made for garbage collection, which can be greatly simplified if only some basic properties (that happen to hold for a majority of all objects and pointers, but not all) can be guaranteed. A good illustrating example of this can be found in Java: each method call in Java must start by performing a null-check on the target even though less than 10% of all variables ever contain null. If it was possible to statically exclude null values with a compile-time guarantee, much time (and energy) would be saved every day on a global scale. A similar argument can be made for thread-safety.
I have supervised a number of theses at Uppsala University, related to programming languages. I supervise both bachelor and master students.
Recent Topics I have Supervised/Reviewed
- 1. Implementation of standard library components for the Encore programming language (Bachelor)
- 2. Prototype implementation of the VAT programming abstraction for Encore (Bachelor)
- 3. Design and implementation of Pattern Matching Support for Encore (Bachelor)
- 4. Type System Support for Lock-Free Data Structures (Bachelor)
- 5. Implementation of Reagents in Encore (Master)
I mostly supervise theses which are related to my research. A somewhat updated list of thesis topic proposals is maintained here.