To reference or cite the objects present in the Software Heritage archive, permalinks based on SoftWare Hash IDentifiers (SWHIDs) must be used. Select below a type of object currently browsed in order to display its associated SWHID and permalink.
swh:1:cnt:fdaac8c22dc02690a0449ae8576df44c7bdfe0ef
swh:1:dir:f716f58574f8ed17a6f1b566f9641ad07912cbf5
# Mi-Cho-Coq A specification of Michelson in Coq to prove properties about smart contracts in Tezos.