K-user mailing list

[Russell Wallace <russell.wallace AT gmail.com>]

Yes, that helps, thanks!

On Fri, Aug 25, 2017 at 4:02 PM, Chen, Xiaohong <xc3 AT illinois.edu> wrote:

Hi Russell,

Good question. As Everett points out, K back-ends allow reachability analysis + operation semantics, which essentially is just matching logic reasoning, since (we suppose that) reachability logic theories can be expressed as matching logic theories. Therefore, I think what you mean by "a runtime model of K" is the inference system (proof system) of matching logic, which you could find in the canonical paper which proposes matching logic.

We have been developing a Semantics of K proposal in which we will eventually define K definitions as matching logic theories (https://github.com/kframework/matching-logic-prover/tree/master/semantics_of_k). Backends will then explain / justify whatever they do with K definitions in terms of matching logic reasoning.

Yours,
Xiaohong

-------------------------
Chen, Xiaohong
BSc, Peking University
PhD student, UIUC

________________________________________
From: Everett Hildenbrandt [hildenb2 AT illinois.edu]
Sent: Friday, August 25, 2017 8:22 AM
To: Russell Wallace
Cc: k-user AT lists.cs.illinois.edu
Subject: Re: [[K-user] ] Runtime object/memory model

K evolved out of Rewriting Logic (the original K-Maude was implemented in Maude, see http://fsl.cs.illinois.edu/index.php/K-Maude:_A_Rewriting_Based_Tool_for_Semantics_of_Programming_Languages).
An inference system for reachability was developed, which made reasoning about program behavior efficient and simple (see Reachability Logic papers, http://fsl.cs.illinois.edu/index.php/Reachability_Logic).
Reachability Logic (which generalizes Hoare Logic) allows you to use whatever static logic you like for representing states, and only describes how to do reachability analysis.
This also allows us to take an operational semantics (eg. a K definition) *directly* as an axiomatic semantics, without having to do some Hoare Logic style proof of equivalence of two semantics.

More recently, we've been working with Matching Logic (originally just the static logic that K used by default, see Matching Logic resources, http://fsl.cs.illinois.edu/index.php/Matching_Logic).
We suppose that perhaps Reachability Logic theories can be expressed as Matching Logic specifications.

In short, I think of K as a very nice symbolic rewriting engine (therefore the underlying data-structures are terms in a term-algebra).
Perhaps Xiaohong Chen can shed some better light on this, as there has been some work towards putting together a document describing the semantics of K in a digestible and rigorous format.

Hope this helps,
Everett H.

On Fri, Aug 25, 2017 at 10:40:11AM +0100, Russell Wallace wrote:
> Just came across K recently, and it looks interesting! The tutorial documents
> and videos I've found so far mostly talk about the front-end, language syntax
> and semantics, which is very impressive, but what I'm particularly interested
> in right now is the runtime object/memory model.
>
> By which I mean, assembly language has a runtime model where everything is a
> big array of bytes, C has one where there are separate memory segments that are
> sort of arrays of bytes but with a bunch of rules about what is and isn't
> defined behavior, in Java everything is an object, Lisp starts with atoms and
> cons cells, but elaborates from there etc.
>
> Where should I be looking for the explanation of the K runtime model?