When writing a compiler for a functional programming language, an important consideration is the treatment of binders and variables. A well-known technique when using dependently typed programming languages such as Agda is to define an intrinsically typed syntax tree, where expressions are scope- and type-safe by construction and admit a total evaluation function. This construction has featured in several papers, exploring basic operations like renaming and substitution as well as compilation to different target languages.

While optimisations play an important role in compilers and establishing their correctness is often not trivial, there has been little focus on performing optimisations on intrinsically typed programs. In this setting, program analysis not only needs to identify optimisation opportunities, but provide a proof witness that the optimisation is safe, e.g. that some dead code is indeed not used. For transformations on intrinsically typed programs, the programmer can rely on the compiler to check the relevant invariants, but it can be cumbersome to make it sufficiently clear that type- and scope-safety are preserved, especially when manipulating binders and variables.

Since our work is still in progress, we will mainly present a specific optimisation, dead binding elimination. It is implemented by first annotating expressions with variable usage information and then removing the bindings that turn out to be unused. We further prove that the optimisation is semantics-preserving.