Compiling Agda to System Fω in Theory
Detta är en Kandidat-uppsats från Göteborgs universitet/Institutionen för data- och informationsteknik
Sammanfattning: 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ω.
HÄR KAN DU HÄMTA UPPSATSEN I FULLTEXT. (följ länken till nästa sida)