K-user mailing list

[Everett Hildenbrandt <hildenb2 AT illinois.edu>]

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?