The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

So, I was reading a bit about matching logic when I came across "Towards a unified theory of axiomatic and operational semantics", and it gave me pause. There a lot that I think I should understand fundamentally.

What basis does Coq work at, technically? I've read seven chapters into Interactive Theorem Proving and Program Development, and I don't think either axiomatic or operational semantics are mentioned anywhere, because I realized that I didn't know which it utilized. Can someone provide some clarification?

And also, I was pretty curious about the article itself. It purports some interesting ease in the difficulty of proofs. Not to say that I am attracted by a shortcut, but the idea of being able to annotate a language item seemed like a major payoff if proofs can be derived from the concrete implementation and checked against the desired properties. Does anybody have any thoughts or points about Matching Logic? It's a very new idea to me, so I'd like to hear anything that anybody has to say about it. There doesn't seem to be an interactive tool that can be downloaded to familiarize myself with their theory as with Coq though :(