| Year | Type | Name | URL |
|---|---|---|---|
| 2003 | Notes | CS322 Fall 2003: Programming Language Design - Lecture Notes – | https://www.ideals.illinois.edu/handle/2142/11385 |
| 2005 | Tech Report | K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation - Version 1 - | https://www.ideals.illinois.edu/handle/2142/11215 |
| 2006 | Tech Report | K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation - Version 2 - | https://www.ideals.illinois.edu/handle/2142/11284 |
| 2007 | Tech Report | K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation - Preliminary Version - | https://www.ideals.illinois.edu/handle/2142/11354 |
| 2010 | Journal Article | An Overview of the K Semantic Framework | https://www.ideals.illinois.edu/handle/2142/14865 (tech report version) |
| Year | Type | K Version | Name | Paper URL | Code URL |
|---|---|---|---|---|---|
| 2005 | Tech Report | N/A | A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters | https://www.ideals.illinois.edu/handle/2142/11129 | ??? |
| 2010 | Tech Report | N/A | On Compiling Rewriting Logic Language Definitions into Competitive Interpreters | https://www.ideals.illinois.edu/handle/2142/17444 | ??? |
| 2010 | Article | V1 | K-Maude: A Rewriting Based Tool for Semantics of Programming Languages | https://link.springer.com/chapter/10.1007%2F978-3-642-16310-4_8 | ??? |
| Version | Year | Frontend Language | Backend Language | Comments |
|---|---|---|---|---|
| N/A | 2003 | Maude | Maude | Implemented as Maude library |
| N/A | 2005 | ??? | C | Semi-automated compiler routine in unknown language |
| N/A | 2010 | Perl | OCaml | Designed for speed |
| V1 | 2010 | Maude | Maude | Designed for research/general use |
| V2 | 2010 | Bash/Perl | Maude | Successor of V1 |
| V3 | 2012 | Java | Maude | Parser implemented in Java SDF |
| V3.1 | 2013 | Java | Maude/Java | Added symbolic Java backend |
Other K Backends:
- OCaml Version
- Scala Version
- Coq Version
- Haskell Version
- LLVM Version
- Java-to-Maude: 7fb626aa8a49f4b17b203835afaeab579b1ae87c : Wed Mar 21 14:42:21 2012
- Kore-to-Haskell: 80110ebbb045f4a95551d0a6685b0dd8989e0b92 : Mon Jan 22 14:54:15 2018
- Kore-to-LLVM: 554391 : Jul 17 2018
Maude Modules - Programs and Languages written in Maude - K1 Original K to Maude - compiler in Perl - K2
krun was first tool rewritten in Java - Maude was still doing parsing kompile was parsed in Java SDF to get AST KIL and then compiled to Maude - everything was in Java - K3
krun/kompile was now fully in Java and main goal was verification - by Andrei Stefanescu - K3.X
-
SDF parser was replaced by a hand-written parser based on scannerless Early parser
-
kompile pipeline was rewitten so that inner parser used new syntax and datastructures (kore legacy) - in K v4
-
Dwight led OCaml backend development - only for concrete execution
-
K project was forked
- K Legacy - K4 was the legacy version of K
- Scala backend that kale
- Java backend was further developed and later merged into modern K
- K Company - K5 was RV version of K
- Scanner parsing using flex
- K Legacy - K4 was the legacy version of K
-
New kore intermediate language was introduced
-
Haskell backend start over from scratch for symbolic execution
-
LLVM backend start over from scartch for concrete execution being even faster
-
OCaml backend was sunsetted because they were running up against limits of the OCaml language
-
GLR parser used in modern K