Dependently typed languages allow developers to enforce compile time correctness of programs via the type system. These guarantees however, have to be proven with code, incurring a runtime and memory overhead. These costs can be avoided by using erasure (based on Quantitative Type Theory (QTT)) to omit code marked as erased (e.g. the aforementioned guarantees), which enables a separation between compile-time and run-time concerns.
Erasure annotations can give rise to types that are nominally different but structurally equal at runtime. We name functions between these types that behave like the identity at runtime, runtime identity (runid) functions. Current solutions do not have a structured way to reason about these runid functions as a first class member of the type system. This means programmers have no way to enforce that the compiler will erase these functions nor use the information of runid status to propagate optimizations, like defining runid functions that are polymorphic on some underlying runid function.
This thesis introduces a lightweight core language that extends a QTT-style, intensional Martin-Löf Type Theory (MLTT) with explicit markers for runid functions. We extend the type system with a static check that ensures runid-marked functions are equivalent to the identity function at run-time, using a novel run-time equivalence relation.
As a secondary contribution, we define a semantics for our language inspired by Normalization by Evaluation (NbE). Our semantic domain is extensional, i.e. function equality is extensional, and agnostic to the compilation target, providing a clean model for reasoning about erased and runtime identity behaviour. We prove the soundness of our static analysis by showing that runid-equivalent terms are mapped to equal semantic values

This paper concerns itself with correct by construction refactoring of Maybe values to List values in a Haskell-like language (HLL) as a case study on data-oriented refactorings. Our language makes use of intrinsically-typed syntax and de Bruijn indices for variables. Operational semantics are defined using big step semantics. We define a refactoring function which intrinsically verifies its well-typedness due to our intrinsically-typed syntax. The semantic validity of this refactoring is given by a separate proof. We use Agda, a functional language and theorem prover, to define and prove these properties. Techniques and concepts used in our refactoring and proof generalize well to other data-oriented refactorings.