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

        LeanWasm: An Intrinsically-Typed Interpreter for WebAssembly

        Thumbnail
        View/Open
        LeanWasm.pdf (419.4Kb)
        Publication date
        2024
        Author
        Ionescu, Alex
        Metadata
        Show full item record
        Summary
        WebAssembly is a new low-level programming language and portable bytecode format designed with the goal of increasing interoperability and security across the software ecosystem. In order to ensure correctness and adherence to the official specification, some WebAssembly implementations use formally verified interpreters as testing oracles. This thesis explores a novel approach to defining verified interpreters, by using an intrinsically-typed representation of the WebAssembly abstract syntax. The main contributions of this thesis include an intrinsically-typed WebAssembly interpreter that closely follows the official reference interpreter, and an optimized interpreter based on an improved representation of control-flow. The interpreters are implemented in the Lean 4 theorem prover, leveraging its support for dependent typing and functional-but-in-place programming.
        URI
        https://studenttheses.uu.nl/handle/20.500.12932/46861
        Collections
        • Theses
        Utrecht university logo