In this paper we present a methodology to organize the construction of a correct compiler, taking advantage of the power of full dependently type systems. The basic idea consists in decorating the abstract syntax of languages with their semantics, allowing to express the correctness of the compiler at type level. We show our methodology in a first small example and then explore how it can be promoted to more realistic languages, realizing that our internalistic approach is feasible for defining a correct-by-construction compiler from an imperative language with conditional iteration to a stack based intermediate language. We also show how this methodology can be combined with the externalist approach, compiling from the intermediate language to an assembly-like low level code and separately proving its correctness.

Abstract We introduce a new formulation of pure type systems (PTSs) with explicit substitution and de Bruijn indices and formally prove some of its meta-theory. Using techniques based on Normalisation by Evaluation, we prove that untyped conversion can be typed for predicative PTSs. Although this equivalence was settled by Siles and Herbelin for the conventional presentation of PTSs, we strongly conjecture that our proof method can also be applied to PTSs with η.