https://gitlab.com/nomadic-labs/mi-cho-coq
Revision 7949fdf0a2a2b8a468c0ab5136050fa65054826c authored by Raphaël Cauderlier on 24 January 2020, 11:03:30 UTC, committed by Raphaël Cauderlier on 24 January 2020, 11:03:30 UTC
Remove the return_to_sender contract See merge request nomadic-labs/mi-cho-coq!54
Tip revision: 7949fdf0a2a2b8a468c0ab5136050fa65054826c authored by Raphaël Cauderlier on 24 January 2020, 11:03:30 UTC
Merge branch 'rafoo@no_return_to_sender' into 'dev'
Merge branch 'rafoo@no_return_to_sender' into 'dev'
Tip revision: 7949fdf
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"
]
Computing file changes ...