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

        Analysis and Transformation of Intrinsically Typed Syntax

        Thumbnail
        View/Open
        thesis-final-matthias-heinzel.pdf (555.1Kb)
        Publication date
        2023
        Author
        Heinzel, Matthias
        Metadata
        Show full item record
        Summary
        The correctness of variable representations used in compilers usually depends on the compiler writers’ diligence to maintain complex invariants. Program transformations that manipulate the binding structure are therefore tricky to get right. In a dependently typed programming language such as Agda, we can however make use of intrinsically typed syntax trees to enforce type- and scope-safety by construction, ruling out a large class of binding-related bugs. We show how to perform (and prove correct) dead binding elimination and let- sinking using intrinsically typed de Bruijn indices. To avoid repeated traversals of the transformed expression, we include variable liveness information into the syntax tree and later employ a co-de-Bruijn representation. Finally, we perform transformations in this style syntax-generically.
        URI
        https://studenttheses.uu.nl/handle/20.500.12932/44219
        Collections
        • Theses
        Utrecht university logo