Revision 3fb4ceb39b4bcbf25a0cba9e9508584b74e2c133 authored by Arvid Jakobsson on 10 March 2020, 14:23:46 UTC, committed by Arvid Jakobsson on 11 March 2020, 13:52:45 UTC
Related to #21
1 parent 00e403d
coq-mi-cho-coq.opam
version: "dev"
opam-version: "2.0"
synopsis: "A specification of Michelson in Coq to prove properties about smart contracts in Tezos"
maintainer: "raphael.cauderlier@nomadic-labs.com"
authors: [ "Raphaƫl Cauderlier" "Bruno Bernardo" "Julien Tesson" "Arvid Jakobsson" ]
homepage: "https://gitlab.com/nomadic-labs/mi-cho-coq/"
dev-repo: "git+https://gitlab.com/nomadic-labs/mi-cho-coq/"
bug-reports: "https://gitlab.com/nomadic-labs/mi-cho-coq/issues"
license: "MIT"
build: [
["./configure"]
[make "-j%{jobs}%"]
]
install: [
make "install"
]
depends: [
"ocamlbuild"
"coq-menhirlib" {>= "20190626"}
"coq-ott" {>= "0.29"}
"coq" {>= "8.8"}
"coq-ott"
"ott"
"menhir"
"coq-menhirlib" {>= "20190626"}
"zarith"
"ocaml" {>= "4.07.1"}
"ott" {build & >= "0.29"}
"zarith"
]
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:Programming Languages/Formal Definitions and Theory"
"keyword:cryptocurrency"
"keyword:michelson"
"keyword:semantics"
"keyword:smart-contract"
"keyword:tezos"
"logpath:Michocoq"
"logpath:Michocott"
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...