k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[[K-user] ] Source-to-source transformations / rule-based optimizations

From: bongiovanni AT gmail.com
To: k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] Source-to-source transformations / rule-based optimizations
Date: Thu, 07 Sep 2017 09:09:40 -0500

Hello,

I would like to have a K expert opinion about a specific usage I have in
mind.

I've been toying with K yet I wonder this thing :

Given any two K formal semantics, let's say, C and ORC, do you think it is
possible (and feasible) to create a K-based source-to-source translator that
would translate a C program into an ORC program while retaining the semantics
of the original C program ?

Did some folks at UUIC work on that by any chances ? is there any interests in
doing such a thing ?

I am also interested in rule-based optimizations with K (Seokje Seo did a nice
Msc thesis about that :
https://www.ideals.illinois.edu/bitstream/handle/2142/88962/SEO-THESIS-2015.pdf?sequence=1),
I tried to replicated his stuff with no success..., is there any proper
documentation regarding the internals of K ?

Thanks in advance !

Cheers !

- Francesco

[[K-user] ] Source-to-source transformations / rule-based optimizations, bongiovanni, 09/07/2017
- Re: [[K-user] ] Source-to-source transformations / rule-based optimizations, Everett Hildenbrandt, 09/08/2017
- Re: [[K-user] ] Source-to-source transformations / rule-based optimizations, Park, Daejun, 09/08/2017
  - Re: [[K-user] ] Source-to-source transformations / rule-based optimizations, Bongiovanni Francesco A., 09/11/2017
    - Re: [[K-user] ] Source-to-source transformations / rule-based optimizations, Park, Daejun, 09/14/2017
      - Re: [[K-user] ] Source-to-source transformations / rule-based optimizations, Daniel Schnetzer Fava, 09/15/2017