The Coq mailing list

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

On Tue, May 31, 2016 at 5:00 PM, Stefan Ciobaca <stefan.ciobaca AT gmail.com> wrote:

I have replied earlier, but I think that the message was eaten away by the system. I believe it clarifies some of the points that were raised. Here is the original message:

First of all, I like to think of Coq as a programming language with a proof assistant on top. It is possible to express in Coq any (terminating) computation and make machine-certified proofs about the computation. The machine-checking is done by a small kernel which does have an operational semantics consists of several reduction rules (beta, iota, zeta, eta, etc. reduction); the kernel is called CIC and it has been shown sound on paper. Coq has numerous success stories, but I believe that one of the more important is that it has been used in the programming language community to give formal semantics to programming languages, make type soundness proofs, etc. I believe other members of the list can provide more valuable insight into this.

Matching logic is about formally defining programming languages and reasoning about programs. The idea is to have *a single operational semantics* for each language; every language tool such as interpreters, compilers, type checkers, deductive verifiers, etc. should be parametric in the language semantics. Therefore, if the semantics changes, (e.g. due to new a language version or a bug fix in the language semantics), the tools automatically change as well. You don't risk your compiler being out-of-sync with e.g. the program verifier. Matching logic is just a natural way to achieve this language-parametricity easily. Therefore, these two approaches to program verification (Coq and Matching Logic) should be seen as orthogonal. For example, I have used Coq to create a machine-checked soundness proof of the matching logic proof system (http://fsl.cs.illinois.edu/index.php/Reachability_Logic_-_Supporting_Material - scroll to the bottom of the page).

|... should be seen as orthogonal. For example, I have used Coq to create a machine-checked soundness proof of the matching logic proof system

Amazing! I thought they were discrete systems and techniques. That's cool they can be used together.

 

Secondly, there are quite a few tools based on matching logic, the most important being the K Framework (http://www.kframework.org/), which allows you to formally define your language; you obtain for free an interpreter, exhaustive state explorer, symbolic execution and program verifier, etc. K has been used to give semantics to C, Java, _javascript_. K is nowhere near the maturity of Coq in terms of stability, but it is being commercialised in the form of an undefinedness runtime checker for C programs (https://runtimeverification.com/match/).

If you want to find out more about matching logic, here are a few papers I recommend:

A bit of history behind the project:

TCS: The Rewriting Logic Semantics Project (Jose Meseguer and Grigore Rosu)

Inf. and Comp.: A rewriting logic approach to operational semantics (Traian Florin Şerbănuţă, Grigore Roşu, José Meseguer)

Papers on matching logic:

LICS 2013: One-Path Reachability Logic (Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, Brandon M. Moore)

RTA 2014: All-Path Reachability Logic (Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-

Florin Serbanuta, Grigore Rosu)

RTA 2015: Matching Logic - Extended Abstract (Invited Talk, Grigore Rosu)


Real language semantics in K:

Chris Hathhorn, Chucky Ellison, Grigore Rosu:
Defining the undefinedness of C. PLDI 2015: 336-345

Daejun Park, Andrei Stefanescu, Grigore Rosu:
KJS: a complete formal semantics of _javascript_. PLDI 2015: 346-356

Denis Bogdanas, Grigore Rosu:
K-Java: A Complete Semantics of Java. POPL 2015: 445-456

Best,
Stefan

On Tue, May 31, 2016 at 9:15 PM, roux cody <cody.roux AT gmail.com> wrote:

To give a brief answer to Thorsten, matching logic (http://www.matching-logic.org/index.php/Matching_Logic) seems to be a "small steps" version of the usual Hoare Logic for proving properties about programs (with state). It seems to be particularly well-suited to prove simple(ish) computational properties of programs with side effects.

Coq, seen as a programing language (sometimes called Gallina) is pure: side effects are not possible (this is even more dramatic than in Haskell, where side effects need to be "hidden" in an IO monad). In effect, a pure language doesn't really need a "program logic": you can directly insert expressions directly into the formulas, and since everything is an _expression_, there's no need for any machinery that handles the extraneous state.

Of course, sometimes we want to represent stateful computations, and there you need some kind of encoding, e.g. along the lines of Haskell's State monad.

On Tue, May 31, 2016 at 1:46 PM, Kenneth Adam Miller <kennethadammiller AT gmail.com> wrote:

Wow!

Thank you so much to all of you.

On May 31, 2016 1:26 PM, "Xavier Leroy" <Xavier.Leroy AT inria.fr> wrote:

On 31/05/16 07:20, Kenneth Adam Miller wrote:
> 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

Just hold tight for a few more chapters!  The chapters Imp, Equiv,
Hoare, Hoare2 and Smallstep explain very well the approach already
mentioned in this thread, namely defining the syntax and (operational or
axiomatic) semantics of a programming language in Coq, and proving
properties about them.

> You can't add a semantics for a language built under and by Coq?

You can certainly define semantics for a programming language in Coq.

> What about Mezzo, there is a language that was built with Coq.

Not really "built with Coq".  Rather, its abstract syntax, operational
semantics and type systems were formalized using Coq, then proved sound.

> If you're right, then I guess that the mezzo source files just map
> down to Coq types eventually.

You could look up the terms "shallow embedding" and "deep embedding"
in the literature.  What you have in mind sounds like a deep embedding
but the Mezzo formalization, and many other P.L. formalizations in
Coq, use the "shallow embedding" approach.

Hope this helps,

- Xavier Leroy