View Item 
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        JavaScript is disabled for your browser. Some features of this site may not work without it.

        Browse

        All of UU Student Theses RepositoryBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

        The Agda UHC Backend

        Thumbnail
        View/Open
        MSc_thesis_Agda_UHC_Backend.pdf (303.8Kb)
        Publication date
        2015
        Author
        Hausmann, P.
        Metadata
        Show full item record
        Summary
        This thesis studies how we can facilitate combined Haskell/Agda developments. As foundation for our research we have created the Agda UHC backend, targeting the intermediate Core language of the Utrecht Haskell Compiler. We will present a formal description of our translation scheme, which now powers all major Agda backends. Building upon our new backend, we introduce a Contract framework specifically aimed at the Foreign Function Interface (FFI). As with most FFI implementations, a major challenge are the different type systems of the languages involved. Our contract library provides a concise and powerful way to translate data between Agda foreign languages like Haskell. We also provide a formal specification of our contract framework, making it feasible to implement a similar scheme in other languages. Furthermore, we provide an improved Agda FFI interface for function calls which combines well with our Contract framework. Our contributions make Agda a more viable choice for applied dependently-typed programming and provide an elegant and novel solution for the FFI problem in a dependently typed setting.
        URI
        https://studenttheses.uu.nl/handle/20.500.12932/28189
        Collections
        • Theses
        Utrecht university logo