package coq-mi-cho-coq
A specification of Michelson in Coq to prove properties about smart contracts in Tezos
Install
Dune Dependency
Authors
Maintainers
Sources
mi-cho-coq-version-1.0.tar.gz
md5=1b939c4ca68af82527b8d60419100557
Description
Michelson is a language for writing smart contracts on the Tezos blockchain. This package provides a Coq encoding of the syntax and semantics of Michelson, automatically generated by the Ott tool. Also included is a framework called Mi-Cho-Coq for reasoning about Michelson programs in Coq using a weakest precondition calculus.
Tags
category:Computer Science/Programming Languages/Formal Definitions and Theory date:2021-06-15 keyword:cryptocurrency keyword:michelson keyword:semantics keyword:smart-contract keyword:tezos logpath:Michocoq logpath:MichocottPublished: 21 Jun 2021
Dependencies (10)
- zarith
-
ott
build & >= "0.29" - ocamlbuild
-
ocaml
>= "4.07.1" - menhir
-
coq
>= "8.10" & < "8.12.0" -
coq-ott
>= "0.29" -
coq-moment
>= "1.2.0" -
coq-menhirlib
>= "20190626" - coq-list-string
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page