Project Proposal

Programmers writing smart contracts for the Ethereum Virtual Machine (EVM) must provide an upper bound for execution cost, and in the event that this bound is incorrect, they may waste gas. Hence, it is desirable to compute this upper bound by static means. My work is to compile to the EVM a language for which such static resource analysis already exists (OCaml).

I am working with Professor Jan Hoffmann of CMU's Principles of Programming (POP) group. His expertise is in formal verification, compiler design, and type systems.

Milestone Reports

Milestone 1

Milestone 2

Milestone 3

Milestone 4

Milestone 5

Milestone 6

Milestone 7