Welcome to the PLTC Section. We perform research in programming language technology and in the theory of computation. Much of our work involves topics in the intersection of programming language theory (e.g., algorithmic aspects of programming and formal verification), and applications (e.g., computer security and privacy, systems, distributed ledger technology, and fintech).
The PLTC Section is located on the ground floor of HCØ, in Building B, Universitetsparken 5, DK-2100 Copenhagen.
We perform research in programming language technology (including ties to program analysis, type systems and transformation, compiler and language design, high-performance computing, and meta-programming), and in the theory of computation (including ties to automata and computability theory, logic, term rewriting and lambda calculus, and reversible and quantum computing).
Much of our work involves topics in the intersection of programming languages and theory (e.g., algorithmic aspects of programming and formal verification), and applications (e.g., computer security and privacy, systems, distributed ledger technology, and Fintech).
We offer courses for the bachelor and master’s programmes in Computer Science, Computer Science and Economics, Machine-learning & Datascience, and Communication & IT. For the MSc programme, we are primarily involved in the study track in Programming Language and Systems.
PLTC researchers conduct project supervision spanning both BSc level and MSc level supervision and spanning all kinds of projects, including thesis projects, POCS (project out of course scope), PREP (thesis preparation project), and projects involving external institutions or companies (for such projects it is in general assumed that students them selves come with collaboration ideas).
Here is an overview of topics and reseacher competences:
Compilation and optimisation. (Torben Mogensen, Cosmin Oancea, Martin Elsman, Troels Henriksen). Related courses: PMPH, PLD, IPS.
Type systems and type inference. (Andrzej Filinski, Troels Henriksen, Martin Elsman, Robert Glück, Torben Mogensen). Related courses: SAT.
Data-parallel and GPU programming. (Cosmin Oancea, Troels Henriksen, Martin Elsman). Related courses: PMPH, DPP.
Reversible languages. (Robert Glück, Torben Mogensen, Michael Kirkedal Thomsen). Related courses: PAT.
Quantum computing. (Fritz Henglein, Martin Elsman, Michael Kirkedal Thomsen). Related courses: ATPL.
High-performance computing. (Cosmin Oancea, James Avery, David Marchant). Related courses: PMPH, COMPSYS, HPPS.
Probabilistic programming. (Thomas Hamelryck). Related courses: …
Security and language-based security. (Boel Nelson, Thomas Jensen, Andrzej Filinski). Related courses: ITS, SOS, PCS.
Systems and hardware-near programming. (Philippe Bonnet). Related courses: COMPSYS, HPPS, ACS, DIS.
Finance, contracts, and distributed systems. (Omry Ross, Fritz Henglein). Related courses: DATFIN, Blockchain.
If you are looking for a BSc project supervisor, please contact one of the above listed researchers, depending on the topic.
Futhark is a research language developed by various PLTC researchers. See this curated list of GitHub issues for suggestions on projects related to working on the compiler itself. Contact Troels Henriksen, Cosmin Oancea, or Martin Elsman if you wish to work on one of thse.
The Problem Based Benchmark Suite is a collection of benchmark programs that implement various algorithms using parallel programming. Currently only implementations for multicore CPUs are supported. It would be interesting to port some of these benchmarks to low-level GPU programming languages, such as CUDA. While some of the benchmark programs are fairly trivial, others are highly irregular and will require some cleverness to implement efficiently on GPUs. This means the size of the project can be adjusted based on the time available. Contact: Troels Henriksen.
