K-user mailing list

["Chen, Xiaohong" <xc3 AT illinois.edu>]

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?