Partial Evaluation in Dependently Typed Languages
Lead Research Organisation:
University of St Andrews
Department Name: Computer Science
Abstract
This project aims to explore the optimisation of dependently typed programming languages using partial evaluation. In addition to answering open research
questions, the project will provide a concrete implementation of a partial evaluator for the Idris2 compiler. The project furthers the research already undertaken by Brady[4], aiming to make dependently typed languages practical for
writing everyday programs through the careful application of program optimisations.
Partial evaluation (PE) is an optimisation technique which evaluates portions
of the program at compile time to produce a more efficient executable[7]. It is a
powerful generalisation of constant folding, which allows programmers to write
idiomatic definitions without loss of performance. Many modern programming
languages implement PE, with some inferring the areas of program to evaluate,
and with others taking explicit guidance from the programmers (for example,
C++11's constexpr keyword). The main drawback to partial evaluation is that
it can be very expensive for large programs, significantly increasing compilation
times.
questions, the project will provide a concrete implementation of a partial evaluator for the Idris2 compiler. The project furthers the research already undertaken by Brady[4], aiming to make dependently typed languages practical for
writing everyday programs through the careful application of program optimisations.
Partial evaluation (PE) is an optimisation technique which evaluates portions
of the program at compile time to produce a more efficient executable[7]. It is a
powerful generalisation of constant folding, which allows programmers to write
idiomatic definitions without loss of performance. Many modern programming
languages implement PE, with some inferring the areas of program to evaluate,
and with others taking explicit guidance from the programmers (for example,
C++11's constexpr keyword). The main drawback to partial evaluation is that
it can be very expensive for large programs, significantly increasing compilation
times.
Organisations
People |
ORCID iD |
Edwin Brady (Primary Supervisor) | |
Ellis Kesterton (Student) |
Studentship Projects
Project Reference | Relationship | Related To | Start | End | Student Name |
---|---|---|---|---|---|
EP/T518062/1 | 01/10/2020 | 30/09/2025 | |||
2589772 | Studentship | EP/T518062/1 | 01/10/2021 | 31/03/2025 | Ellis Kesterton |