K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

Dear Corey,

Thanks for your interest in K.  Nice to hear the tutorials were useful, 
because they took a lot of time to put together.  We are now under a heavy 
transition to K 4.0, where the tutorial will need to be all redone, too, in 
addition to several of the K tools.

I would say now it is an excellent time to develop an Isabelle backend!  The 
wiki on KORE has not been updated yet, but the KORE itself is getting to a 
point where it is reliably stable.  Cosmin (the K lead developer at UIUC) 
would probably say that it is already there.  We still need to update the 
wiki documentation, though.

I am CC-ing Elsa Gunter, who has a student who started developing an Isabelle 
backend for K.  Not sure if it is working with K4.0 or with the entire K, but 
I believe that it would be good for you two (you and Elsa's student) to 
discuss over hangouts and see what the current status is.

Note that we also have an OCAML backend in my startup company 
(runtimeveritication.com) that powers our RV-Match tool; if needed, we can 
show you how that works, too, provided you sign an NDA.

Ideally, it would be nice to have a common infrastructure for 
functional-style backends (OCAML, Isabelle, Coq, Haskell, etc).  Let us know 
if you want to get deeper into this (but we should likely leave the k-user 
list out, to not spam everybody).

Best,
Grigore



________________________________________
From: Corey Richardson 
[corey AT octayn.net]
Sent: Saturday, April 30, 2016 11:49 PM
To: 
k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] K2Isabelle

Greetings,

K looks like a very excellent tool for working with semantics. The
tutorials and documentation are excellent, far better than is the norm
for these sorts of tools.

I see that there is a project idea for an Isabelle backend as a
"Summer+" project. I am interested in at least starting work on such a
backend in about a month or so.

I'm have a few kuestions:

- I read some of the wiki and issues about KAST/KORE.  It seems that
  work is still ongoing. Is soon a good time to start on a new backend
  at all, given those (seemingly invasive) changes to the innards?

- I notice that at least large parts of KORE seem to be written in
  Scala. Is Scala the implementation language of choice?

- Does anyone have concrete ideas for what the output of such a backend
  would look like? In particular, I can imagine deeply embedding the
  actions of the rewrite rules over some generated datatypes, or deeply
  embedding K's flavour of rewrite logic.

  I imagine the decision the Coq backend makes would be relevant. Are
  there instructions on how to set up and use that?

Best,
--
cmr
+610481782084
http://octayn.net/