- Advanced Programming (AP)
- Computability and Complexity (CoCo)
- Data-Driven Financial Models (DatFin)
- Parallel Functional Programming (PFP)
- Proactive Computer Security (PCS)
- Program Analysis and Transformation (PAT)
- Programming Massively Parallel Hardware (PMPH)
- Semantics and Types (SaT)
Topics in Programming Languages (TiPL)
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.
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.
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).
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.