Skip to main content

Exam



Question 1#

What is returned by the execution of a smart contract ?











Question 2#

What makes the bridge between the Tezos world and the formal world of Coq ?







Question 3#

Who is Thierry Coquand ?







Question 4#

We have seen that a Michelson script must be translated into an annotated script (i.e. a formal definition) (because Mi-Cho-Coq provides an equivalent for each Michelson instruction). In the theorem we want to prove, we specify that "the execution of the annotated script is equivalent to post-conditions". Who is responsible for the execution of this annotated script ?






Question 5#

What post-conditions depends on (What post-conditions are built upon) ?










Last updated on by Aymeric BETHENCOURT