https://gitlab.com/nomadic-labs/mi-cho-coq
Revision 241569172d52cf882f8fd8e7398fb914a5d75226 authored by Raphaël Cauderlier on 26 April 2020, 20:07:01 UTC, committed by Raphaël Cauderlier on 14 May 2020, 19:39:36 UTC
This uses `Bool.Is_true (negb ...)` instead of `... = false` in the definition of the `mutez` type which simplifies a bit reasoning about the implementation of mutez.
1 parent 93912f6
Tip revision: 241569172d52cf882f8fd8e7398fb914a5d75226 authored by Raphaël Cauderlier on 26 April 2020, 20:07:01 UTC
[michocoq] Simplification of tez.v
[michocoq] Simplification of tez.v
Tip revision: 2415691
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: [
"coq-list-string"
"coq-menhirlib" {>= "20190626"}
"coq-moment" {>= "1.2.0"}
"coq-ott" {>= "0.29"}
"coq" {>= "8.8"}
"menhir"
"ocaml" {>= "4.07.1"}
"ocamlbuild"
"ott" {build & >= "0.29"}
"zarith"
]
build-test: [ make "test" ]
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 ...