Compiling Agda to System Fω in Theory

dc.contributor.author	Ulm, Gregor
dc.date.accessioned	2015-07-20T13:07:22Z
dc.date.available	2015-07-20T13:07:22Z
dc.date.issued	2015-07-20
dc.identifier.uri	http://hdl.handle.net/2077/39972
dc.description.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ω.	sv
dc.language.iso	eng	sv
dc.subject	Languages	sv
dc.subject	Lambda calculus and related systems	sv
dc.subject	Types	sv
dc.subject	Compilers	sv
dc.title	Compiling Agda to System Fω in Theory	sv
dc.type	text
dc.setspec.uppsok	Technology
dc.type.uppsok	M2
dc.contributor.department	Göteborgs universitet/Institutionen för data- och informationsteknik	swe
dc.contributor.department	University of Gothenburg/Department of Computer Science and Engineering	eng
dc.type.degree	Student essay