K-user mailing list

[Corey Richardson <corey AT octayn.net>]

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/

Attachment: signature.asc
Description: PGP signature