The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

2016-05-31 18:14 GMT+02:00 Kenneth Adam Miller <kennethadammiller AT gmail.com>:

On Tue, May 31, 2016 at 12:06 PM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

Kenneth I think you are mixing two levels of "semantics" that have almost nothing to do one with another:

1) Coq underlying theory (CIC) which is the very heart of Coq itself, whose "semantics" (i.e. logical model) justify Coq as a sound proof system. This semantics are very strange and complex mathematical objects that I myself don't understand.

2) The semantics (axiomatic, operational, whatever) you can define INSIDE coq. These are Coq *definitions* (like functions in a programming language). There are litterally hundreds of such semantics around written in Coq. Most of these are rather simple objects and can be defined without caring about CIC's semantics.

Makes much more sense now.

 

I am pretty sure that matching logic can be defined in Coq as another kind of semantics.

Fascinating. I wonder if a project could look at extricating some judiciously limited portion of Matching Logic semantics from individual statements in a particular language automatically. (Not pre and post conditions, or invariants, but just to assist the user in a custom driven fashion). Then the user would need only take care to ensure that the gap between intention and need is filled.

This sounds like everyday work of some coq users. See for example:

http://www.chargueraud.org/softs/cfml/

for something that sounds like what you have in mind, but with "characteristic formlae" instead of "matching logic judgements".

P.