package coq-mi-cho-coq

  1. Overview
  2. No Docs
A specification of Michelson in Coq to prove properties about smart contracts in Tezos

Install

Dune Dependency

gitlab.com Edit opam file Versions (2)

Authors

  1. R
    Raphaël Cauderlier
  2. B
    Bruno Bernardo
  3. J
    Julien Tesson
  4. A
    Arvid Jakobsson

Maintainers

  1. R
    raphael.cauderlier@nomadic-labs.com

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:Michocott

Published: 21 Jun 2021

Dependencies (10)

  1. zarith
  2. ott build & >= "0.29"
  3. ocamlbuild
  4. ocaml >= "4.07.1"
  5. menhir
  6. coq >= "8.10" & < "8.12.0"
  7. coq-ott >= "0.29"
  8. coq-moment >= "1.2.0"
  9. coq-menhirlib >= "20190626"
  10. coq-list-string

Dev Dependencies

None

Used by

None

Conflicts

None