[Haskell] PhD fellowships in ”Parallel functional programming” and "Systems-level language-based security"

[Troels Henriksen]

Full information, including deadlines and such:

https://di.ku.dk/ominstituttet/ledige_stillinger/phd-fellowships-in-parallel-functional-programming-and-systems-level-language-based-security/

The section for Programming Languages and the Theory of Computation
(PLTC) at the Department of Computer Science invites applicants for PhD
fellowships in two areas: data parallel programming languages broadly
construed (including design, implementation, theoretical aspects, and
parallel algorithms), and the intersection of systems-level security and
formal aspects of computer science (e.g., verification, type systems,
programming languages, language-based security, formal methods, logic
and so on). When applying, please indicate which areas are of interest
to you (which can be both).

Two positions, are available:

# Parallel Functional Programming

Parallel programming on modern massively parallel processors such as
GPUs is notoriously difficult and awkward for humans, particularly for
irregular problems or those with nested structure. At DIKU, we are a
small team that researches programming and compilation techniques for
making high-performance parallel programming more accessible to
non-specialist programmers. We conduct applied research with a focus on
actual real-world performance on mainstream hardware, and we use the
functional array language Futhark (https://futhark-lang.org) and its
implementation as our main experimental vessel. The precise research
problems to be investigated by the PhD candidate depends on the
interests of the candidate, but we are particularly interested in
problems such as:

 * How to efficiently map fully or partially irregular nested
   parallelism to hardware, while still taking advantage of locality.

 * The construction of profiling tools that can precisely measure the
   performance of heavily compiler-transformed code and connect it to
   the original program, allowing the programmer to understand the
   high-level performance of their program.

 * Optimising data layout based on how it is accessed by the program;
   possibly also taking distributed execution or NUMA behaviour into
   account.

 * Data parallel formulations of algorithms that are historically
   difficult to express; e.g. syntax analysis, constraint propagation,
   and similar recursive and irregular problems.

At a basic level, our research consists of developing a strong idea, and
then demonstrating the applicability of the idea by implementing it in a
practically usable compiler or tool. For more information, feel free to
contact Troels Henriksen (athas at diku.dk).

# Systems-Level Language-Based Security

Systems-level security is a challenging field, particularly because it
is often difficult to fully ensure the absence of errors. For example,
modern operating systems use kernel extensions provided by users to add
functionalities like network filters and performance tracking. These
extensions, while useful, can pose significant security risks as they
run with high privileges, potentially affecting the entire system or can
access sensitive information. At DIKU, we are a small group that
researches programming-language techniques and formal methods for
improving systems-level security. We conduct both applied research and
theoretical work, with Open Source software such as the Linux kernel as
one of our main interests.

The specific research areas for the PhD candidate will align with their
interests. However, we're particularly keen on exploring topics such as:

 * Providing strong, formally verified security guarantees for the eBPF subsystem in the Linux kernel.

 * Using user-provided code, like WebAssembly or eBPF, for computational storage, ensuring these have strong security guarantees.

 * Using the programming language Rust for improving systems-level Open
   Source project, for instance the Linux kernel. Hereunder, exploring
   automated verification of Rust code correctness, including the
   development of, or contribution to existing tools for reasoning about
   Rust code.

Our research typically involves developing a solid idea and
demonstrating its practical application, either through a usable tool or
a proof-of-concept. For more information, feel free to contact Ken Friis
Larsen (kflarsen at di.ku.dk).