tezoscoq
tezoscoq copied to clipboard
tezos
working with coq and tezos
Hello! I'd like to prove correctness of a few simple Michelson programs in Coq. Since the language specification has changed in the last two years, (i) which branch should I...
There is no license information on this repository or in any the source code files. Is it meant to be published eventually with the same license as Tezos itself?
It might be nice to have tezoscoq published in the nice Coq OPAM repository for projects which depend on it. http://coq.io/opam/
Right now instructions are typed against a stack, while programs are not: `Inductive has_prog_type : program -> instr_type -> Prop := ` `with has_instr_type : instr -> stack -> instr_type...
Right now stack type is defined as `with stack_type := | empty_stack : stack_type | cons_stack : type -> stack_type -> stack_type ` but it should be something as close...