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

        Formalizing Extended UTxO and BitML Calculus in Agda

        Thumbnail
        View/Open
        thesis.pdf (330.9Kb)
        Publication date
        2019
        Author
        Melkonian, O.
        Metadata
        Show full item record
        Summary
        Smart contracts – programs that run on a blockchain – allow for sophisticated transactional schemes, but their concurrent execution makes it difficult to reason about their behaviour and bugs in smart contracts have lead to significant monetary losses (e.g. DAO attack). For that reason, increasingly more attention is given to formal methods, that guarantee that such fatal scenarios are not possible. We attempt to advance the state-of-the-art for a language-oriented, type-driven account of smart contracts by formalizing two well-established models in Agda and mechanizing the corresponding meta-theory. The first concerns an abstract model for UTxO-based ledgers, such as Bitcoin, which we further extend to cover features of the Cardano blockchain, namely more expressive scripts and built-in support for user-issued cryptocurrencies. The second object of study is BitML, a process calculus specifically targeting Bitcoin smart con- tracts. We present a mechanized semantics of BitML contracts and its small-step semantics, as well as a mechanized account of BitML’s symbolic model over participant strategies. Finally, we sketch the way towards a certified compiler from BitML contracts to UTxO transac- tions, where all behaviours manifesting on BitML’s symbolic model can safely be transported to the UTxO level.
        URI
        https://studenttheses.uu.nl/handle/20.500.12932/32981
        Collections
        • Theses
        Utrecht university logo