Programming Languages and Theory of Computation (PLTC)

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

• Decentralized Systems

  We research and develop foundations, technology and applications of efficient and secure networked/distributed computer systems controlled by multiple independent principals.  This includes blockchain and distributed ledger technology, event-driven architectures, large-scale transaction processing and analytics (Big Data), streaming and real-time data processing, domain-specific languages embodying domain knowledge and deep computer science techniques, digital and smart contract technology, and more.
  More info about the group TBA

• Security & Privacy

  We work primarily on software-based security and privacy preservation techniques and applications. Emerging research topics are quantum cryptography and compositional safety and security models for industrial systems.
  More info about the group TBA

• HOT Lab

  We design and develop theoretical and practical aspects of advanced Higher-Order and Typed programming language technology. Examples include type-based analyses and domain-specific languages.
  More info about the group TBA

• Program Inversion and Reversible Computing

  We study reversible computing with a focus on garbage-free computation models and design of programming languages in these. Relations to other areas include categorical models, IT-security, computer systems, and quantum computation.
  More info about the group TBA

• Programming Language Theory and Technology

  Our research covers theoretical and practical research of programming languages with a focus on automatic program optimization, analysis and transformation.
  More info about the group TBA

• Theory of Computation

  We conduct primarily theoretical research into the nature of computing. The aim is to prove universal results concerning the problems that can, and particularly, cannot be solved by computers or other computing devices.
  More info about the group TBA

• Functional Technology for Modern Architectures (FUTHARK)

  We conduct language and compiler research, particularly with respect to using functional techniques for generating efficient code for modern high-performance architectures, including GPUs and multicore CPUs.
  More info about the group TBA

Partial Evaluator for Datatype Generic Programming (MSc Thesis)

Datatype generic programming is a technique for developing algorithms that work for many datatypes by relying on structural information about their definition. For example, one could implement generic printing, equality, ordering, enumeration, functor and traversable.

There is however a substantial overhead in running these algorithms using the general representation of programs.  In order to speed up execution time and memory consumption, we would like to implement a partial evaluator algorithm we have sketched out. This removes the static part of the overhead by specializing implementations for different instantiations.

Contact: Ahmad Salim Al-Sibahi, Assistant Professor

Compiled Implementation of Strong Reduction for Idris or Agda (MSc Thesis)

Dependently typed languages like Idris and Agda often have a conversion rule for type checking, which requires evaluating expressions at type-checking time. This implementation must support evaluation of open terms, in addition to closed terms, since they often appear in types.

Traditional implementation of evaluators can be slow for complex types, which rely on heavy computation at type-checking time. Gregoire and Leroy have designed an algorithm which relies on JIT compilation for efficient evaluation. We would like to port this algorithm to dependent type systems like Idris or Agda.

Contact: Ahmad Salim Al-Sibahi, Assistant Professor

Implementation of extensional type theory (XTT) or observational type theory (OTT) for Idris 2 (MSc Thesis)

Idris 2 is a practical programming language that relies on dependent types for expressivity. The equality type is however not very strong and does not work well with functions. This can make it hard to prove laws of common type classes like functors, applicative and monads.

We would like to implement a more expressive equality for Idris 2 based on either extensional type theory (XTT) or observational type theory (OTT).

Contact: Ahmad Salim Al-Sibahi, Assistant Professor

A Widening Algorithm for Relational Inductive Refinement Types (MSc Thesis)

Many program transformation languages work primarily with inductive data-types. We have implemented a static analysis for these languages, which can capture inductive invariants to reason about the correctness of programs like refactorings, compilers, desugarings, evaluators and type checkers.

However, our analysis does not support capturing relational information between elements, and so plenty of information is lost. We would like to develop a widening algorithm that extends our implementation to support relational information between elements, e.g., allowing us to prove that a tree has a smaller value in its left subtree than its right subtree.

Contact: Ahmad Salim Al-Sibahi, Assistant Professor