Compiling Agda to System Fω in Theory
No Thumbnail Available
Date
2015-07-20
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
We develop a theoretical foundation for compiling the programming
language Agda to System Fω, which is a stepping stone towards
a compiler from Agda to Haskell. The practical relevance
for software engineering and the problem of providing correctness
guarantees for programs is highlighted. After describing relevant λ-
calculi, we specify the semantics for compiling Agda to System Fω.
Finally, we illustrate those compilation rules by manually translating
several Agda code examples to System Fω.
Description
Keywords
Languages, Lambda calculus and related systems, Types, Compilers