Title: Mechanizing the Semantics of Tezos’ Bytecode in F*

Abstract:  In this presentation from 2017, I will recall work done during an internship towards the mechanization of the semantics of Michelson, the opcode language of the Tezos cryptocurrency, using the F* theorem prover. Partial correctness of simple contracts was achieved. We managed to cross-compile of our Fstar code with the rest of the Tezos Ocaml codebase and confront it to their standard benchmarks.

About the speaker: Thomas Sibut-Pinote is a PhD student at Inria Saclay/École Polytechnique https://specfun.inria.fr/~tsibutpi/

About the talk: The talk is open to everyone interested and is organized by the Concordium Blockchain Research Center Aarhus. For further information about the research center, please visit the center website: http://cs.au.dk/research/centers/concordium/