The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

As far as I understand, Coq's foundation is orthogonal to matching logic, which is not nearly strong enough to formalize all of math.  The reduction semantics of Coq (in the definitional equality) can be viewed as an operational semantics, though.  If you want to learn more, you might want to read Software Foundations.

On 05/31/2016 01:20 AM, Kenneth Adam Miller wrote:

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 :(