Verified Translation of a Strongly Typed Functional Language with Variables to a Language of Indexed Gates

Abstract

In this thesis, we present a translation from an embedded hardware description language with variable bindings (lambda one) to an embedded hardware description language without variable bindings (Piware). The host language for these embedded languages is Agda. We take a look at type theory and how it relates to higher order logic according to the Curry-Howard isomorphism, at different ways to implement variable binding and finally at the translation itself. Not only do we show how to translate to a nameless language, but we also present a correctness proof of said translation formalized in Agda itself.