k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] K2Isabelle

From: Corey Richardson <corey AT octayn.net>
To: k-user AT lists.cs.illinois.edu
Subject: Re: [[K-user] ] K2Isabelle
Date: Sun, 1 May 2016 14:54:21 +1000

On Sun, May 01, 2016 at 02:49:59PM +1000, Corey Richardson wrote:
> - 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.
>

Shallowly embedding K's flavour of rewrite logic, that is.

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

Attachment: signature.asc
Description: PGP signature

[[K-user] ] K2Isabelle, Corey Richardson, 04/30/2016
- Re: [[K-user] ] K2Isabelle, Corey Richardson, 04/30/2016