diff --git a/API/src/main/java/org/kframework/Kapi.java b/API/src/main/java/org/kframework/Kapi.java
index d023f2a0bf..c305079599 100644
--- a/API/src/main/java/org/kframework/Kapi.java
+++ b/API/src/main/java/org/kframework/Kapi.java
@@ -335,7 +335,7 @@ public static Info getInfo(CompiledDefinition compiledDef, String proofFile, Str
         List<Rule> specRulesKORE = stream(specModule.localRules())
                 .filter(r -> r.toString().contains("spec.k"))
                 .map(r -> (Rule) macroExpander.expand(r))
-                .map(r -> ProofExecutionMode.transformFunction(JavaBackend::ADTKVariableToSortedVariable, r))
+                .map(r -> ProofExecutionMode.transformFunction(Kompile::ADTKVariableToSortedVariable, r))
                 .map(r -> ProofExecutionMode.transformFunction(Kompile::convertKSeqToKApply, r))
                 .map(r -> ProofExecutionMode.transform(NormalizeKSeq.self(), r))
                         //.map(r -> kompile.compileRule(compiledDefinition, r))
@@ -485,7 +485,7 @@ public void kprove(String proofFile, String prelude, CompiledDefinition compiled
         List<Rule> specRules = stream(specModule.localRules())
                 .filter(r -> r.toString().contains("spec.k"))
                 .map(r -> (Rule) macroExpander.expand(r))
-                .map(r -> ProofExecutionMode.transformFunction(JavaBackend::ADTKVariableToSortedVariable, r))
+                .map(r -> ProofExecutionMode.transformFunction(Kompile::ADTKVariableToSortedVariable, r))
                 .map(r -> ProofExecutionMode.transformFunction(Kompile::convertKSeqToKApply, r))
                 .map(r -> ProofExecutionMode.transform(NormalizeKSeq.self(), r))
                         //.map(r -> kompile.compileRule(compiledDefinition, r))
diff --git a/frontend/pom.xml b/frontend/pom.xml
index 001f383eb8..29512afd15 100644
--- a/frontend/pom.xml
+++ b/frontend/pom.xml
@@ -48,7 +48,7 @@
     <dependency>
       <groupId>org.kframework.k</groupId>
       <artifactId>kore_2.12</artifactId>
-      <version>1.0-SNAPSHOT</version>
+      <version>0.6-SNAPSHOT</version>
     </dependency>
   </dependencies>
 
diff --git a/frontend/src/main/java/org/kframework/builtin/KLabels.java b/frontend/src/main/java/org/kframework/builtin/KLabels.java
index c623ca2a47..5dc210bcb6 100644
--- a/frontend/src/main/java/org/kframework/builtin/KLabels.java
+++ b/frontend/src/main/java/org/kframework/builtin/KLabels.java
@@ -26,5 +26,5 @@ public class KLabels {
 
     public static final String GENERATED_TOP_CELL = "generatedTop";
     public static final String THIS_CONFIGURATION = "THIS_CONFIGURATION";
-    public static final String MAP_LOOKUP = "Map:lookup";
+    public static final String MAP_LOOKUP = "Map@MAP.lookup";
 }
diff --git a/frontend/src/main/scala/org/kframework/minikore/converters/KoreToMini.scala b/frontend/src/main/scala/org/kframework/minikore/converters/KoreToMini.scala
index f1ef711442..13a318ad9b 100644
--- a/frontend/src/main/scala/org/kframework/minikore/converters/KoreToMini.scala
+++ b/frontend/src/main/scala/org/kframework/minikore/converters/KoreToMini.scala
@@ -1,6 +1,7 @@
 package org.kframework.minikore.converters
 
-import org.kframework.kore._
+import org.kframework.attributes.Att
+import org.kframework.kore.{Sort, _}
 import org.kframework.kore.implementation.DefaultBuilders
 import org.kframework.frontend.SortedADT.SortedKVariable
 import org.kframework.frontend.Unapply._
@@ -40,8 +41,17 @@ object KoreToMini {
       })
       val newAtt = items.map(encode) ++ apply(att)
       prod.klabel match {
-        case Some(label) => SymbolDeclaration(b.Sort(sort.name), b.Symbol(label.name), args, Attributes(newAtt))
-        case None => SymbolDeclaration(b.Sort(sort.name), iNone, args, Attributes(newAtt)) // TODO(Daejun): either subsort or regex; generate injection label for subsort; dummy sentence for regex
+        case Some(label) if label.name != "" =>
+          SymbolDeclaration(b.Sort(sort.name), b.Symbol(label.name), args, Attributes(newAtt))
+        case _ =>
+          if (att.contains(Att.token)) {
+            SymbolDeclaration(b.Sort(sort.name), b.Symbol(sort.name), args, Attributes(newAtt))
+          } else {
+            assert(args.size == 1)
+            val subsort: Sort = args.head
+            SymbolDeclaration(b.Sort(sort.name), b.Symbol("#inject_" + subsort.str + "_into_" + sort.name), args, Attributes(newAtt)) // TODO(Daejun): either subsort or regex; generate injection label for subsort; dummy sentence for regex
+          }
+
       }
 
     case definition.Rule(body, requires, ensures, att) =>
@@ -126,7 +136,7 @@ object KoreToMini {
   // encodePatternAtt(p, Seq(a1,a2,a3)) = #(#(#(p,a1),a2),a3) // TODO(Daejun): add test
   def encodePatternAtt(p: Pattern, att: Attributes): Pattern = {
     att.patterns.foldLeft(p)((z, a) => {
-      b.Application(iAtt, Seq(z, a))
+      b.Application(DefaultBuilders.knownSymbols.PatternWithAttributes, Seq(z, a))
     })
   }
 
@@ -169,9 +179,6 @@ object KoreToMini {
     Symbol("#None"))
   val encodingLabels = encodingLabelTuple.productIterator.toSet
 
-  val iAtt = Symbol("#")
   val iKSeq = Symbol("#kseq")
   val iKSeqNil = Symbol("#kseqnil")
-
-  val iNone = Symbol("#None")
 }
diff --git a/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala b/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala
index 1295a1f614..ddf72049a6 100644
--- a/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala
+++ b/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala
@@ -4,10 +4,11 @@ import org.kframework.frontend.SortedADT.SortedKVariable
 import org.kframework.frontend.{KORE, _}
 import org.kframework.{attributes, definition}
 import org.kframework.kore._
+
 import scala.collection.JavaConverters._
 import scala.collection._
-
 import KoreToMini._
+import org.kframework.kore.implementation.DefaultBuilders
 
 object MiniToKore {
 
@@ -19,18 +20,21 @@ object MiniToKore {
     val origModuleMap: Map[String, Module] = seq2map(d.modules)
 
     val mainModuleName = findAtt(d.att, iMainModule.str) match {
-      case Seq(DomainValue(Symbol("S"), Value(name))) => name; case _ => ???
+      case Seq(DomainValue(Symbol("S"), Value(name))) => name;
+      case _ => ???
     }
     val (mainModules, otherModules) = d.modules.partition(m => m.name.str == mainModuleName)
-    val mainModule = mainModules.head; assert(mainModules.size == 1)
+    val mainModule = mainModules.head;
+    assert(mainModules.size == 1)
 
     val entryModules = findAtt(d.att, iEntryModules.str).map({
-      case DomainValue(Symbol("S"), Value(name)) => origModuleMap(name); case _ => ???
+      case DomainValue(Symbol("S"), Value(name)) => origModuleMap(name);
+      case _ => ???
     })
 
     val newModuleMapRef: mutable.Map[String, definition.Module] = mutable.Map.empty // will dynamically grow during translating modules
-    val newMainModule = apply(origModuleMap,newModuleMapRef)(mainModule)
-    val newEntryModules = entryModules.map(apply(origModuleMap,newModuleMapRef))
+    val newMainModule = apply(origModuleMap, newModuleMapRef)(mainModule)
+    val newEntryModules = entryModules.map(apply(origModuleMap, newModuleMapRef))
     definition.Definition(
       newMainModule,
       newEntryModules.toSet,
@@ -41,7 +45,7 @@ object MiniToKore {
   def apply(origModuleMap: Map[String, Module], newModuleMapRef: mutable.Map[String, definition.Module])
            (m: Module): definition.Module = {
     val imports = m.sentences.collect({
-      case Import(name, _) => findOrGenModule(origModuleMap,newModuleMapRef)(name.str)
+      case Import(name, _) => findOrGenModule(origModuleMap, newModuleMapRef)(name.str)
     })
     val sentences = m.sentences.filter({ case Import(_, _) => false; case _ => true })
     definition.Module(m.name.str, imports.toSet, sentences.map(apply).toSet, apply(m.att))
@@ -51,7 +55,7 @@ object MiniToKore {
                      (name: String): definition.Module = {
     if (newModuleMapRef.contains(name)) newModuleMapRef(name)
     else {
-      val m = apply(origModuleMap,newModuleMapRef)(origModuleMap(name))
+      val m = apply(origModuleMap, newModuleMapRef)(origModuleMap(name))
       newModuleMapRef += (name -> m)
       m
     }
@@ -84,7 +88,8 @@ object MiniToKore {
       val priorities = prios.map({
         case Application(`iSyntaxPriorityGroup`, group) =>
           group.map({
-            case DomainValue(Symbol("S"), Value(tag)) => definition.Tag(tag); case _ => ???
+            case DomainValue(Symbol("S"), Value(tag)) => definition.Tag(tag);
+            case _ => ???
           }).toSet
         case _ => ???
       })
@@ -97,7 +102,8 @@ object MiniToKore {
         case _ => ???
       }
       val ts = tags.map({
-        case DomainValue(Symbol("S"), tag) => definition.Tag(tag.str); case _ => ???
+        case DomainValue(Symbol("S"), tag) => definition.Tag(tag.str);
+        case _ => ???
       }).toSet
       definition.SyntaxAssociativity(assoc, ts, apply(att))
     case Application(`iBubble`, Seq(DomainValue(Symbol("S"), Value(sentence)), DomainValue(Symbol("S"), Value(contents)))) +: att =>
@@ -111,7 +117,8 @@ object MiniToKore {
 
   def apply(att: Seq[Pattern]): attributes.Att = {
     def isDummy(p: Pattern): Boolean = p match {
-      case Application(l, _) => encodingLabels.contains(l); case _ => false
+      case Application(l, _) => encodingLabels.contains(l);
+      case _ => false
     }
     attributes.Att(att.filterNot(isDummy).map(apply).toSet)
   }
@@ -119,7 +126,7 @@ object MiniToKore {
   def apply(p: Pattern): K = apply(attributes.Att())(p)
 
   def apply(att: attributes.Att)(p: Pattern): K = p match {
-    case Application(`iKSeq`, Seq(p1,p2)) =>
+    case Application(`iKSeq`, Seq(p1, p2)) =>
       apply(p2) match {
         case k2: KSequence =>
           val items = apply(p1) +: k2.items.asScala.toList // from KSequence in Unapply.scala
@@ -129,16 +136,17 @@ object MiniToKore {
     case Application(`iKSeqNil`, Seq()) =>
       ADT.KSequence(List(), att)
 
-    case Application(`iAtt`, Seq(p1,p2)) =>
+    case Application(DefaultBuilders.knownSymbols.PatternWithAttributes, Seq(p1, p2)) =>
       val a2 = apply(Seq(p2))
       apply(att ++ a2)(p1)
 
     case Application(Symbol(label), args) => KORE.KApply(KORE.KLabel(label), args.map(apply), att)
+
     case DomainValue(Symbol(label), Value(value)) => KORE.KToken(value, KORE.Sort(label), att)
     case SortedVariable(Name(name), Sort("_")) => KORE.KVariable(name, att)
     case SortedVariable(Name(name), _) => SortedKVariable(name, att)
     case Rewrite(left, right) => KORE.KRewrite(apply(left), apply(right), att)
-    case _ => ???
+    case _ => throw new AssertionError("Implementation missing. Couldn't match: " + p + " of class " + p.getClass)
   }
 
   def findAtt(att: Attributes, key: String): Seq[Pattern] = {
diff --git a/frontend/src/test/scala/org/kframework/minikore/KoreToMiniTest.scala b/frontend/src/test/scala/org/kframework/minikore/KoreToMiniTest.scala
index 57a985ced5..b2a9c04c9a 100644
--- a/frontend/src/test/scala/org/kframework/minikore/KoreToMiniTest.scala
+++ b/frontend/src/test/scala/org/kframework/minikore/KoreToMiniTest.scala
@@ -30,7 +30,7 @@ class KoreToMiniTest {
   @Test def production2(): Unit = {
     assertEquals(
       apply(new definition.Production(Exp, Seq(NonTerminal(Int)), Att())),
-      SymbolDeclaration(Sort(Exp.name), Symbol("#None"), Seq(Sort(Int.name)), Attributes(Seq(Application(iNonTerminal, Seq(S(Int.name))))))
+      SymbolDeclaration(Sort(Exp.name), Symbol("#inject_Int@INT-SYNTAX_into_Exp@A-SYNTAX"), Seq(Sort(Int.name)), Attributes(Seq(Application(iNonTerminal, Seq(S(Int.name))))))
     )
   }
 
diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaBackend.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaBackend.java
index 7fce18c7d6..6ec8184242 100644
--- a/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaBackend.java
+++ b/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaBackend.java
@@ -109,7 +109,7 @@ public Function<Definition, Definition> steps() {
                 .andThen(expandMacrosDefinitionTransformer::apply)
                 .andThen(DefinitionTransformer.fromSentenceTransformer(new NormalizeAssoc(KORE.c()), "normalize assoc"))
                 .andThen(convertDataStructureToLookup)
-                .andThen(DefinitionTransformer.fromRuleBodyTranformer(JavaBackend::ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable"))
+                .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile::ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable"))
                 .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile::convertKSeqToKApply, "kseq to kapply"))
                 .andThen(DefinitionTransformer.fromRuleBodyTranformer(NormalizeKSeq.self(), "normalize kseq"))
                 .andThen(JavaBackend::markRegularRules)
@@ -132,7 +132,7 @@ public Function<Definition, Definition> stepsForProverRules() {
                 .andThen(AddBottomSortForListsWithIdenticalLabels.singleton().lift())
                 .andThen(DefinitionTransformer.fromKTransformerWithModuleInfo(JavaBackend::moduleQualifySortPredicates, "Module-qualify sort predicates"))
                 .andThen(expandMacrosDefinitionTransformer::apply)
-                .andThen(DefinitionTransformer.fromRuleBodyTranformer(JavaBackend::ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable"))
+                .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile::ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable"))
                 .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile::convertKSeqToKApply, "kseq to kapply"))
                 .andThen(DefinitionTransformer.fromRuleBodyTranformer(NormalizeKSeq.self(), "normalize kseq"))
                 .andThen(JavaBackend::markRegularRules)
@@ -157,17 +157,6 @@ private static Definition markRegularRules(Definition d) {
         }, "mark regular rules").apply(d);
     }
 
-    /**
-     * The Java backend expects sorted variables, so transform them to the sorted flavor.
-     */
-    public static K ADTKVariableToSortedVariable(K ruleBody) {
-        return new TransformK() {
-            public K apply(KVariable kvar) {
-                return new SortedADT.SortedKVariable(kvar.name(), kvar.att());
-            }
-        }.apply(ruleBody);
-    }
-
     /**
      * Replace variables which only appear once in the pattern and have no side condition on them (including no sorting),
      * with a special marker called THE_VARIABLE which the backend uses for special speed optimisations.
diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java
index c0c969b5e5..7f538e3fbe 100644
--- a/java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java
+++ b/java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java
@@ -153,7 +153,7 @@ public K apply(KVariable k) {
                         cellPlaceholderSubstitutionApplication.apply(r.ensures()),
                         r.att()))
                 .map(r -> (Rule) macroExpander.expand(r))
-                .map(r -> transformFunction(JavaBackend::ADTKVariableToSortedVariable, r))
+                .map(r -> transformFunction(Kompile::ADTKVariableToSortedVariable, r))
                 .map(r -> transformFunction(Kompile::convertKSeqToKApply, r))
                 .map(r -> transform(NormalizeKSeq.self(), r))
                 //.map(r -> kompile.compileRule(compiledDefinition, r))
diff --git a/java-backend/src/main/scala/MiniKoreUtils.scala b/java-backend/src/main/scala/MiniKoreUtils.scala
index 32bd55fdc2..ab72447a7d 100644
--- a/java-backend/src/main/scala/MiniKoreUtils.scala
+++ b/java-backend/src/main/scala/MiniKoreUtils.scala
@@ -62,7 +62,8 @@ object MiniKoreUtils {
       val filterSet = Set(iTerminal.str, iNonTerminal.str, iRegexTerminal.str)
       val labelDecsMap: Map[String, Seq[Pattern]] =
         allSentences collect {
-          case SymbolDeclaration(_, Symbol(label), _, Attributes(att)) if label != iNone => (label, att)
+          // TODO: may need to handle subsort declarations separately
+          case SymbolDeclaration(_, Symbol(label), _, Attributes(att)) => (label, att)
         } groupBy { x => x._1 } mapValues { z => z map {_._2} } mapValues {_.flatten}
       labelDecsMap.mapValues({ s =>
         s.flatMap({ p =>
@@ -139,7 +140,7 @@ object MiniKoreUtils {
 
   def decodePatternAttributes(p: Pattern): (Pattern, Seq[Pattern]) = {
     p match {
-      case Application(`iAtt`, Seq(pat, att)) => decodePatternAttributes(pat) match {
+      case Application(Symbol("#"), Seq(pat, att)) => decodePatternAttributes(pat) match {
         case (finalPat, attList) => (finalPat, attList :+ att)
       }
       case any@_ => (any, Seq())
diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k
index 11b28ad6c7..e93e1c9075 100644
--- a/k-distribution/include/builtin/domains.k
+++ b/k-distribution/include/builtin/domains.k
@@ -24,7 +24,7 @@ module MAP
   imports LIST
   imports SET
 
-  syntax Map [hook(MAP.Map)]
+  syntax Map
 
   /*@\section{Description} The Map represents a generalized associative array.
    Each key can be paired with an arbitrary value, and can be used to reference
@@ -32,24 +32,24 @@ module MAP
 
   /*@ Construct a new Map consisting of key/value pairs of two Maps (the keys of
    the two Maps are assumed disjoint) */
-  syntax Map ::= Map Map                        [left, function, hook(MAP.concat), klabel(_Map_), assoc, comm, unit(.Map), element(_|->_), index(0)]
+  syntax Map ::= Map Map                        [left, function, hook(MAP.concat,.Map(),Int@INT-SYNTAX("0")), klabel(Map@MAP), assoc, comm, unit(.Map), element(_|->_), index(0)]
   /*@  Construct an empty Map */
-  syntax Map ::= ".Map"                         [function, hook(MAP.unit), latex(\dotCt{Map})]
+  syntax Map ::= ".Map"                         [function, latex(\dotCt{Map}), klabel(.Map)]
                // breaks klabel uniqueness
                //| "."                            [function, hook(MAP.unit)]
   syntax Map ::= "(" Map ")" [bracket]
   /*@ Construct a singleton Map (a Map with only one key/value pair). The key
    is on the left and the value is on the right */
-  syntax Map ::= K "|->" K                      [function, hook(MAP.element), latex({#1}\mapsto{#2})]
+  syntax Map ::= K "|->" K                      [latex({#1}\mapsto{#2})]
 
-  syntax priorities _|->_ > _Map_ .Map
+  syntax priorities _|->_ > Map@MAP .Map
   syntax non-assoc _|->_
 
   /*@ Retrieve the value associated with the given key */
-  syntax K ::= Map "[" K "]"                    [function, hook(MAP.lookup), klabel(Map:lookup), relativeHook(_Map_.lookup)]
+  syntax K ::= Map "[" K "]"                    [function, hook(MAP.lookup), klabel(Map@MAP.lookup)]
 
   /*@ Update a Map in form of  of keys and values: */
-  syntax Map ::= Map "[" K "<-" K "]"           [function, hook(MAP.update), prefer]
+  syntax Map ::= Map "[" K "<-" K "]"           [function, hook(MAP.update, label("_|->_")), prefer]
 
   /*@ Remove key/value pair associated with the key from map? */
   syntax Map ::= Map "[" K "<-" "undef" "]"     [function, hook(MAP.remove)]
@@ -67,7 +67,7 @@ module MAP
   syntax Map ::= removeAll(Map, Set)            [function, hook(MAP.removeAll)]
 
   /*@ Get a Set consisting of all keys in the Map:*/
-  syntax Set ::= keys(Map)                      [function, hook(MAP.keys), relativeHook(_Map_.keys)]
+  syntax Set ::= keys(Map)                      [function, hook(MAP.keys), klabel(Map@MAP.keys)]
 
   syntax Bool ::= K "in_keys" "(" Map ")"       [function, hook(MAP.in_keys)]
 
@@ -89,15 +89,16 @@ module SET
   imports BASIC-K
   imports BOOL-SYNTAX
 
-  syntax Set [hook(SET.Set)]
+  syntax Set
 
   /*@ \section{Description} The Set represents a mathematical set (a collection
    of unique items). */
 
   /*@ Construct a new Set as the union of two different sets ($A \cup B$) */
-  syntax Set ::= Set Set                  [left, function, hook(SET.concat), klabel(_Set_), assoc, comm, unit(.Set), idem, element(SetItem)]
+  // TODO: .Set here needs to be the element of an empty set
+  syntax Set ::= Set Set                  [left, function, hook(SET.concat,.Set()), klabel(Set@SET), assoc, comm, unit(.Set), idem, element(SetItem)]
   /*@ Construct an empty Set */
-  syntax Set ::= ".Set"                   [function, hook(SET.unit), latex(\dotCt{Set})]
+  syntax Set ::= ".Set"                   [function, latex(\dotCt{Set})]
                //| "."
   syntax Set ::= "(" Set ")" [bracket]
   /*@ Construct a singleton Set (a Set with only one element $\{ a \}$). To add
@@ -112,7 +113,7 @@ module SET
   syntax Set ::= Set "-Set" Set           [function, hook(SET.difference), latex({#1}-_{\it Set}{#2}), klabel(Set:difference)]
 
   /*@ Check element membership in a set ($a \in A$) */
-  syntax Bool ::= K "in" Set              [function, hook(SET.in), klabel(Set:in), relativeHook(_Set_.in)]
+  syntax Bool ::= K "in" Set              [function, hook(SET.in), klabel(Set@SET.in)]
 
   /*@ Check set inclusion ($A \subseteq B$) */
   syntax Bool ::= Set "<=Set" Set         [function, hook(SET.inclusion)]
@@ -135,7 +136,7 @@ module LIST
   imports BASIC-K
   imports BOOL-SYNTAX
 
-  syntax List [hook(LIST.List)]
+  syntax List
 
   /*@ \section{Description} \K lists are ordered collections that may contain
    duplicate elements. These behave more like lists in functional programming
@@ -168,9 +169,10 @@ module LIST
 
   /*@ Construct a new List as the concatenation of two Lists. This is similar to
    the append "@" operation in many functional programming languages. */
-  syntax List ::= List List               [left, function, hook(LIST.concat), klabel(_List_), smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem)]
+   // TODO: .Set here needs to be the element of an empty list
+  syntax List ::= List List               [left, function, hook(LIST.concat,.List()), klabel(List@LIST), smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem)]
   /*@ Construct an empty List: */
-  syntax List ::= ".List"                 [function, hook(LIST.unit), smtlib(smt_seq_nil), latex(\dotCt{List})]
+  syntax List ::= ".List"                 [function, smtlib(smt_seq_nil), latex(\dotCt{List})]
                 //| "."
   /*@ Construct a singleton List (a list with only  one element) */
   syntax List ::= ListItem(K)             [smtlib(smt_seq_elem)]
@@ -193,9 +195,9 @@ endmodule
 module BOOL-SYNTAX
   imports SORT-K
 
-  syntax Bool [hook(BOOL.Bool)]
-  syntax Bool ::= "true"  [token]
-  syntax Bool ::= "false" [token]
+  syntax Bool
+  syntax Bool ::= "true"  [hook(BOOL.Bool), token]
+  syntax Bool ::= "false" [hook(BOOL.Bool), token]
 endmodule
 
 module BOOL
@@ -251,8 +253,8 @@ module BOOL
 endmodule
 
 module INT-SYNTAX
-  syntax Int [hook(INT.Int)]
-  syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token]
+  syntax Int
+  syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, hook(INT)]
 endmodule
 
 module INT
@@ -317,10 +319,10 @@ module INT
 endmodule
 
 module FLOAT-SYNTAX
-  syntax Float [hook(FLOAT.Float)]
-  syntax Float ::= r"([\\+\\-]?[0-9]+(\\.[0-9]*)?|\\.[0-9]+)([eE][\\+\\-]?([0-9]+(\\.[0-9]*)?|\\.[0-9]+))?([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token]
-  syntax Float ::= r"[\\+\\-]?Infinity([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token]
-  syntax Float ::= r"NaN([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token]
+  syntax Float
+  syntax Float ::= r"([\\+\\-]?[0-9]+(\\.[0-9]*)?|\\.[0-9]+)([eE][\\+\\-]?([0-9]+(\\.[0-9]*)?|\\.[0-9]+))?([fFdD]|([pP][0-9]+[xX][0-9]+))?" [hook(FLOAT.Float), token]
+  syntax Float ::= r"[\\+\\-]?Infinity([fFdD]|([pP][0-9]+[xX][0-9]+))?" [hook(FLOAT.Float), token]
+  syntax Float ::= r"NaN([fFdD]|([pP][0-9]+[xX][0-9]+))?" [hook(FLOAT.Float), token]
 endmodule
 
 module FLOAT
@@ -401,8 +403,8 @@ module STRING-SYNTAX
   //              | [\\][u] 4*Hex // "\uFFFF"     Backslash 'u' followed by four  hexadecimal characters
   //              | [\\][U] 8*Hex // "\UFFffFFff" Backslash 'U' followed by eight hexadecimal characters
   //                              // the code must not be in the range [0xdfff, 0xd800] or exceed 0x10ffff
-  syntax String [hook(STRING.String)]
-  syntax String ::= r"[\\\"](([^\\\"\n\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]"      [token]
+  syntax String
+  syntax String ::= r"[\\\"](([^\\\"\n\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]"      [token, hook(STRING.String)]
 endmodule
 
 module STRING
@@ -431,8 +433,8 @@ module STRING
   syntax Int    ::= String2Int   ( String )             [function, hook(STRING.string2int)]
   syntax String ::= Int2String   ( Int )                [function, hook(STRING.int2string)]
   syntax String ::= Base2String  ( Int , Int )          [function, hook(STRING.base2string)]
-  syntax Int    ::= String2Base  ( String , Int )       [function, hook(STRING.string2base)]
-  syntax KItem  ::= "#parseToken"  "(" String "," String ")"  [function, hook(STRING.string2token)]
+  syntax Int    ::= String2Base  ( String , Int )       [function, hook(String.string2base)]
+  syntax KItem  ::= "#parseToken"  "(" String "," String ")"  [function, hook(String.string2token)]
 
 
   syntax String ::= "replaceAll" "(" String "," String "," String ")"      [function, hook(STRING.replaceAll)]
@@ -759,13 +761,13 @@ module MINT
   imports K-EQUAL
   imports LIST
 
-  syntax MInt [hook(MINT.MInt)]
+  syntax MInt
 
   /*@\section{Description} The MInt implements machine integers of arbitrary
    * bit width represented in 2's complement. */
 
   /*@ Machine integer of bit width and value. */
-  syntax MInt ::= mi(Int, Int)    [function, hook(MINT.constructor)]
+  syntax MInt ::= mi(Int, Int)    [function, hook(MINT.constructor), klabel(MInt)]
 
   /*@ Function returning the bit width of this machine integer. */
   syntax Int ::= bitwidthMInt(MInt)   [function, hook(MINT.bitwidth)]
diff --git a/k-distribution/include/builtin/kast.k b/k-distribution/include/builtin/kast.k
index 320181a67f..1d727be92b 100644
--- a/k-distribution/include/builtin/kast.k
+++ b/k-distribution/include/builtin/kast.k
@@ -13,7 +13,7 @@ module BASIC-K
   syntax KLabel
   syntax KItem            [hook(K.KItem)]
   syntax K     ::= KItem  [allowChainSubsort]
-  syntax KConfigVar
+  syntax KConfigVar ::= r"(?<![A-Za-z0-9_\\$!\\?])(\\$)([A-Z][A-Za-z0-9'_]*)"          [token, autoReject]
   syntax KBott
   syntax KList
   syntax KResult
@@ -68,7 +68,7 @@ endmodule
 module KSEQ-SYMBOLIC
   imports KSEQ
   syntax #KVariable ::= r"(?<![A-Za-z0-9_\\$!\\?])(\\!|\\?)?([A-Z][A-Za-z0-9'_]*|_)"   [token, autoReject, hook(org.kframework.kore.KVariable)]
-  syntax KConfigVar ::= r"(?<![A-Za-z0-9_\\$!\\?])(\\$)([A-Z][A-Za-z0-9'_]*)"          [token, autoReject]
+
   syntax KBott      ::= #KVariable [allowChainSubsort]
   syntax KBott      ::= KConfigVar [allowChainSubsort]
   syntax KLabel     ::= #KVariable [allowChainSubsort]
diff --git a/k-distribution/pom.xml b/k-distribution/pom.xml
index b3fa4254d5..1163d44732 100644
--- a/k-distribution/pom.xml
+++ b/k-distribution/pom.xml
@@ -50,13 +50,13 @@
     </dependency>
     <dependency>
       <groupId>org.kframework.k</groupId>
-      <artifactId>kale-backend</artifactId>
+      <artifactId>skala-backend</artifactId>
       <version>${project.version}</version>
     </dependency>
     <dependency>
-      <groupId>org.kframework.kale</groupId>
+      <groupId>org.kframework</groupId>
       <artifactId>kale_2.12</artifactId>
-      <version>0.4-SNAPSHOT</version>
+      <version>0.6-SNAPSHOT</version>
     </dependency>
   </dependencies>
 
diff --git a/k-distribution/tutorial/1_k/2_imp/lesson_1/tests/sum.imp b/k-distribution/tutorial/1_k/2_imp/lesson_1/tests/sum.imp
index 23e8bb6df0..fefbfdc3b9 100644
--- a/k-distribution/tutorial/1_k/2_imp/lesson_1/tests/sum.imp
+++ b/k-distribution/tutorial/1_k/2_imp/lesson_1/tests/sum.imp
@@ -2,7 +2,7 @@
 // the sum of numbers from 1 to n.
 
 int n, sum;
-n = 100;
+n = 50;
 sum = 0;
 while (!(n <= 0)) {
   sum = sum + n;
diff --git a/kale-backend/src/main/scala/org/kframework/kale/Hook.scala b/kale-backend/src/main/scala/org/kframework/kale/Hook.scala
deleted file mode 100644
index 7579adb0b3..0000000000
--- a/kale-backend/src/main/scala/org/kframework/kale/Hook.scala
+++ /dev/null
@@ -1,35 +0,0 @@
-package org.kframework.kale
-
-object Hook {
-  def apply(hookName: String, labelName: String)(implicit env: Environment): Option[Label] = {
-    import env.builtin.{INT, BOOLEAN}
-    Some(hookName) collect {
-      case "INT.le" => Operator(labelName, INT, BOOLEAN, (a: Int, b: Int) => a <= b)
-      case "INT.add" => PrimitiveFunction2(labelName, INT, (a: Int, b: Int) => a + b)
-      case "INT.tdiv" => PrimitiveFunction2(labelName, INT, (a: Int, b: Int) => a / b)
-      case "INT.ne" => Operator(labelName, INT, BOOLEAN, (a: Int, b: Int) => a != b)
-      case "BOOL.and" => PrimitiveFunction2[Boolean](labelName, BOOLEAN, _ && _)
-      case "BOOL.or" => PrimitiveFunction2[Boolean](labelName, BOOLEAN, _ || _)
-      case "BOOL.not" => PrimitiveFunction1[Boolean](labelName, BOOLEAN, !_)
-      case "SET.unit" => assert(labelName == ".Set"); env.builtin.BuiltinSetUnit
-      case "SET.concat" => assert(labelName == "_Set_"); env.builtin.BuiltinSet
-    }
-  }
-
-  def relativeHook(relativeHook: String)(implicit env: Environment): Option[Label] = relativeHook.split('.').toSeq match {
-    case Seq(baseLabel: String, hookName: String) => relativeHookByBaseLabel(baseLabel, hookName)
-    case _ => None
-  }
-
-  def relativeHookByBaseLabel(baseLabel: String, hookName: String)(implicit env: Environment): Option[Label] = env.label(baseLabel) match {
-    case l: env.builtin.MapLabel => hookName match {
-      case "lookup" => Some(l.lookup)
-      case "keys" => Some(l.keys)
-      case _ => None
-    }
-    case s: env.builtin.SetLabel => hookName match {
-      case "in" => Some(s.in)
-    }
-    case _ => None
-  }
-}
diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleConverters.scala b/kale-backend/src/main/scala/org/kframework/kale/KaleConverters.scala
deleted file mode 100644
index 9cb2579917..0000000000
--- a/kale-backend/src/main/scala/org/kframework/kale/KaleConverters.scala
+++ /dev/null
@@ -1,89 +0,0 @@
-package org.kframework.kale
-
-import org.kframework.builtin.Sorts
-import org.kframework.definition.Module
-import org.kframework.frontend
-import org.kframework.frontend._
-
-import scala.collection.Map
-
-class KaleConverters(m: Module)(implicit val env: Environment) {
-
-  import env._
-  import env.builtin._
-
-  private val emptyKSeq = FreeLabel0(".K")(env)
-  private val kseq = new AssocWithIdListLabel("~>", emptyKSeq())
-
-  val klabelToLabelRename = Map(
-    "keys" -> "_Map_.keys",
-    "lookup" -> "_Map_.lookup",
-    "Set:in" -> "_Set_.in",
-    "Map:lookup" -> "_Map_.lookup"
-  )
-
-  val labelToKLabelRename = klabelToLabelRename.map(p => (p._2, p._1)).toMap
-
-  def renames(labelName: String) = klabelToLabelRename.getOrElse(labelName, labelName)
-
-  def kSortOf(t: Term): Option[frontend.Sort] =
-    if (!t.isGround)
-      None
-    else
-      m.sortFor
-        .get(KORE.KLabel(t.label.name))
-        .orElse(
-          t.label match {
-            case tokenLabel: GENERIC_TOKEN => Some(m.resolve(frontend.KORE.Sort(tokenLabel.sort.name)))
-            case BOOLEAN => Some(m.resolve(Sorts.Bool))
-            case INT =>
-              Some(m.resolve(Sorts.Int))
-            case STRING => Some(m.resolve(Sorts.String))
-            case `kseq` => Some(m.Sort("KItem"))
-            case `emptyKSeq` => Some(m.Sort("K"))
-            // TODO: handle sorting for conjunctions
-            //            case And =>
-            //              val nonFormulas = And.asSubstitutionAndTerms(t)._2.filter(!_.label.isInstanceOf[FormulaLabel])
-            //              if (nonFormulas.size == 1)
-            //                kSortOf(nonFormulas.head)
-            //              else
-            //                ??? // we have more than one non-formula term. computer the least sort?
-            case Variable => None
-          })
-
-  private lazy val uninterpretedTokenLabels: Map[Sort, ConstantLabel[String]] = (labels collect {
-    case l@GENERIC_TOKEN(s) => (s, l)
-  }).toMap + (Sort("KConfigVar@BASIC-K") -> GENERIC_TOKEN(Sort("KConfigVar@BASIC-K")))
-
-  def convert(klabel: KLabel): Label = label(klabelToLabelRename.getOrElse(klabel.name, klabel.name))
-
-  def convert(body: K): Term = body match {
-    case Unapply.KToken(s, sort) => sort match {
-      case Sorts.Bool => BOOLEAN(s.toBoolean)
-      case Sorts.Int => INT(s.toInt)
-      case Sorts.String => STRING(s)
-      case _ => uninterpretedTokenLabels(Sort(sort.name))(s)
-    }
-    case Unapply.KApply(klabel, list) if klabel.name == "#KSequence" => kseq(list map convert)
-    case Unapply.KApply(klabel, list) => convert(klabel).asInstanceOf[NodeLabel](list map convert)
-    case v: KVariable => Variable(v.name)
-    //      val kaleV = Variable(v.name)
-    //      v.att.get(Att.sort)
-    //        .map(sort => env.And(
-    //          kaleV,
-    //          Equality(env.label("is" + sort.name).asInstanceOf[Label1](kaleV), BOOLEAN(true)))
-    //        )
-    //        .getOrElse(kaleV)
-    case r: KRewrite => Rewrite(convert(r.left), convert(r.right))
-  }
-
-  def convertBack(l: Label): KLabel = KORE.KLabel(labelToKLabelRename.getOrElse(l.name, l.name))
-
-  def convertBack(term: Term): K = term match {
-    case Variable(x) => KORE.KVariable(x)
-    case emptyKSeq() => KORE.KSequence()
-    case t@Node(`kseq`, _) => KORE.KSequence(kseq.asList(t).toList map convertBack: _*)
-    case Node(label, subterms) => KORE.KApply(convertBack(label), (subterms map convertBack).toSeq: _*)
-    case t@Constant(label, value) => KORE.KToken(value.toString, kSortOf(t).get)
-  }
-}
diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala
deleted file mode 100644
index c194e5ac5b..0000000000
--- a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala
+++ /dev/null
@@ -1,210 +0,0 @@
-package org.kframework.kale
-
-import java.util
-import java.util.Optional
-
-import org.kframework.attributes.Att
-import org.kframework.definition._
-import org.kframework.frontend.Unapply.KRewrite
-import org.kframework.frontend._
-import org.kframework.rewriter.SearchType
-import org.kframework.{RewriterResult, frontend}
-
-import scala.collection._
-
-object KaleRewriter {
-  val self = this
-
-  def apply(m: Module): KaleRewriter = new KaleRewriter(m)
-
-  private def isEffectivelyAssoc(att: Att): Boolean =
-    att.contains(Att.assoc) || att.contains(Att.bag)
-}
-
-class KaleRewriter(m: Module) extends org.kframework.rewriter.Rewriter {
-
-  private val productionWithUniqueKLabel: Set[Sentence] = (m.sentences.collect({
-    case p: Production if p.klabel.isDefined => p
-  }) groupBy {_.klabel.get} map {_._2.head}).toSet
-
-  private val syntaxSortDeclarations: Set[Sentence] = m.sentences.collect({
-    case p: SyntaxSort => p
-  }) toSet
-
-  private val assocProductions: Set[Sentence] = productionWithUniqueKLabel.filter(p => KaleRewriter.isEffectivelyAssoc(p.att)).toSet
-
-  private val nonAssocProductions = (productionWithUniqueKLabel | syntaxSortDeclarations) &~ assocProductions
-
-  implicit val env = Environment()
-
-  import env._
-  import env.builtin._
-
-  val converters = new KaleConverters(m)
-
-  import converters._
-
-  case class IsSort(s: Sort)(implicit val env: Environment) extends Named("is" + s.name) with PurelyFunctionalLabel1 with FormulaLabel {
-    def f(_1: Term): Option[Term] =
-      kSortOf(_1).map(ss => BOOLEAN(m.subsorts.<=(ss, m.resolve(frontend.KORE.Sort(s.name)))))
-  }
-
-  private val nonAssocLabels: Set[Label] = nonAssocProductions flatMap {
-    case SyntaxSort(s, att) => None
-    case p@Production(s, items, att) if !att.contains(Att.relativeHook) =>
-      implicit val envv = env
-      att.get(Att.hook)
-        .flatMap({ hookName: String => Hook(hookName, p.klabel.get.name) }) // use the hook if there
-        .orElse({
-        if (att.contains(Att.token)) {
-          // it is a token, but not hooked
-          if (!env.labels.exists(l => l.name == "TOKEN_" + s.name))
-            Some(GENERIC_TOKEN(Sort(s.name)))
-          else
-            None
-        } else {
-          if (p.klabel.isDefined) {
-            val nonTerminals = items.filter(_.isInstanceOf[NonTerminal])
-            val label = if (att.contains(Att.Function)) {
-              if (p.klabel.get.name.startsWith("is")) {
-                IsSort(Sort(p.klabel.get.name.substring(2)))
-              } else {
-                nonTerminals match {
-                  case Seq() => FunctionDefinedByRewritingLabel0(p.klabel.get.name)(env)
-                  case Seq(_) => FunctionDefinedByRewritingLabel1(p.klabel.get.name)(env)
-                  case Seq(_, _) => FunctionDefinedByRewritingLabel2(p.klabel.get.name)(env)
-                  case Seq(_, _, _) => FunctionDefinedByRewritingLabel3(p.klabel.get.name)(env)
-                  case Seq(_, _, _, _) => FunctionDefinedByRewritingLabel4(p.klabel.get.name)(env)
-                }
-              }
-            } else {
-              nonTerminals match {
-                case Seq() => FreeLabel0(p.klabel.get.name)
-                case Seq(_) => FreeLabel1(p.klabel.get.name)
-                case Seq(_, _) => FreeLabel2(p.klabel.get.name)
-                case Seq(_, _, _) => FreeLabel3(p.klabel.get.name)
-                case Seq(_, _, _, _) => FreeLabel4(p.klabel.get.name)
-              }
-            }
-            Some(label)
-          } else
-            None
-        }
-      })
-    case _ => None
-  }
-
-  private val nonConstantLabels: Map[String, NodeLabel] = nonAssocLabels collect {
-    case l: NodeLabel => (l.name, l)
-  } toMap
-
-  def getLabelForAtt(p: Production, att: String): Label = {
-    val labels = nonAssocLabels.filter(l => l.name == p.att.get[String](att).get)
-    assert(labels.size == 1)
-    labels.head
-  }
-
-  assocProductions foreach {
-    case p@Production(s, items, att) =>
-      val unitLabel = getLabelForAtt(p, "unit").asInstanceOf[Label0]
-      val opLabelName = p.klabel.get.name
-      env.uniqueLabels.getOrElse(opLabelName, {
-        val index = att.get[String]("index")
-        if (index.isDefined && att.contains(Att.comm)) {
-          def indexFunction(t: Term): Term = t.iterator().toList(index.get.toInt)
-          MapLabel(opLabelName, indexFunction, unitLabel())(env)
-        } else {
-          new AssocWithIdListLabel(opLabelName, unitLabel())(env)
-        }
-      })
-  }
-
-  nonAssocProductions collect {
-    case p@Production(s, items, att) if att.contains(Att.relativeHook) =>
-      Hook.relativeHook(att.get(Att.relativeHook).get)(env)
-  }
-
-  val functionRulesAsLeftRight: Set[(Label, Rewrite)] = m.rules collect {
-    case rule@Rule(KRewrite(l@Unapply.KApply(klabel, _), r), requires, ensures, att)
-      if m.attributesFor(klabel).contains(Att.`Function`) =>
-      val res = (env.label(klabel.name), Rewrite(And(convert(l), Equality(convert(requires), BOOLEAN(true))), convert(r)))
-      res
-  }
-
-  val functionRules: Map[Label, Set[Rewrite]] = functionRulesAsLeftRight groupBy (_._1) map { case (k, set) => (k, set.map(_._2)) }
-
-  val functionRulesWithRenamedVariables: Map[Label, Set[Rewrite]] = functionRules map { case (k, v) => (k, v map env.renameVariables) }
-
-  env.seal()
-
-  def setFunctionRules(functionRules: Map[Label, Set[Rewrite]]) {
-    env.labels.collect({
-      // TODO: Add an warning for when a function is not defined by either a hook or rules
-      case l: FunctionDefinedByRewriting => l.setRules(functionRules.getOrElse(l, Set()))
-    })
-  }
-
-  setFunctionRules(functionRulesWithRenamedVariables)
-
-  def reconstruct(inhibitForLabel: Label)(t: Term): Term = t match {
-    case Node(label, children) if label != inhibitForLabel => label(children map reconstruct(inhibitForLabel) toIterable)
-    case t => t
-  }
-
-  def resolveFunctionRHS(functionRules: Map[Label, Set[Rewrite]]): Map[Label, Set[Rewrite]] = {
-    functionRules map { case (label, rewrites) => (label, rewrites map (rw => reconstruct(label)(rw).asInstanceOf[Rewrite])) } toMap
-  }
-
-  val finalFunctionRules = Util.fixpoint(resolveFunctionRHS)(functionRules)
-  setFunctionRules(finalFunctionRules)
-
-  val rules: Set[Rewrite] = m.rules collect {
-    case rule@Rule(KRewrite(l@Unapply.KApply(klabel, _), r), requires, ensures, att)
-      if !att.contains(Att.`macro`) && !m.attributesFor(klabel).contains(Att.`Function`) =>
-      val rw = Rewrite(And(convert(l), Equality(convert(requires), BOOLEAN(true))), convert(r))
-      rw
-  }
-
-  val matcher = Matcher(env).default
-  val substitutionApplier = SubstitutionApply(env)
-  val rewriterConstructor = Rewriter(substitutionApplier, matcher, env) _
-
-  // TODO: log this information cleanly
-  //  println("\nFunction rules\n")
-  //  finalFunctionRules.foreach({ case (l, rules) => println(l); println(rules.map("  " + _).mkString("\n")) })
-  //  println("\nRewriting rules\n")
-  //  println(rules.mkString("\n"))
-
-  val rewrite = rewriterConstructor(rules)
-
-  override def execute(k: K, depth: Optional[Integer]): RewriterResult = {
-    var i = 0
-    var term: Term = null
-    var next: Term = convert(k)
-    while (term != next && depth.map[Boolean](i == _).orElse(true)) {
-      term = next
-      next = rewrite.step(term).headOption.getOrElse(term)
-      i += 1
-    }
-    term = next
-    new RewriterResult(Optional.of(0), convertBack(term))
-  }
-
-  override def `match`(k: K, rule: Rule): K = {
-    val kaleO = convert(k)
-    val kaleRule = rule match {
-      case rule@Rule(KRewrite(l@Unapply.KApply(klabel, _), r), requires, ensures, att) =>
-        val rw = Rewrite(And(convert(l), Equality(convert(requires), BOOLEAN(true))), convert(r))
-        rw
-    }
-    val res = matcher(kaleRule._1, kaleO)
-    convertBack(res)
-  }
-
-
-  override def search(initialConfiguration: K, depth: Optional[Integer], bound: Optional[Integer], pattern: Rule, searchType: SearchType, resultsAsSubstitution: Boolean): K = ???
-
-  override def executeAndMatch(k: K, depth: Optional[Integer], rule: Rule): (RewriterResult, K) = ???
-
-  override def prove(rules: util.List[Rule]): util.List[K] = ???
-}
diff --git a/kernel/src/main/java/org/kframework/backend/Backends.java b/kernel/src/main/java/org/kframework/backend/Backends.java
index cbdf4b0c34..37898baab1 100644
--- a/kernel/src/main/java/org/kframework/backend/Backends.java
+++ b/kernel/src/main/java/org/kframework/backend/Backends.java
@@ -8,7 +8,7 @@ public class Backends {
     public static final String DOC = "doc";
     public static final String HTML = "html";
     public static final String JAVA = "java";
-    public static final String KALE = "kale";
+    public static final String SKALA = "skala";
 
     public static final String AUTOINCLUDE_JAVA = "autoinclude-java.k";
 }
diff --git a/kernel/src/main/java/org/kframework/kil/DataStructureSort.java b/kernel/src/main/java/org/kframework/kil/DataStructureSort.java
index 1f7e560cb8..6a25e5d04c 100644
--- a/kernel/src/main/java/org/kframework/kil/DataStructureSort.java
+++ b/kernel/src/main/java/org/kframework/kil/DataStructureSort.java
@@ -4,6 +4,7 @@
 import com.google.common.collect.ImmutableMap;
 import com.google.common.collect.ImmutableSet;
 import org.kframework.kil.loader.Context;
+import org.kframework.kore.implementation;
 
 import java.io.Serializable;
 import java.util.Map;
@@ -64,15 +65,8 @@ public enum Label { CONSTRUCTOR, ELEMENT, UNIT }
     public static final Sort DEFAULT_LIST_SORT = Sort.LIST;
     public static final Sort DEFAULT_MAP_SORT = Sort.MAP;
     public static final Sort DEFAULT_SET_SORT = Sort.SET;
-    public static final String DEFAULT_LIST_LABEL = "_List_";
     public static final String DEFAULT_LIST_ITEM_LABEL = "ListItem";
-    public static final String DEFAULT_LIST_UNIT_LABEL = ".List";
-    public static final String DEFAULT_MAP_LABEL = "_Map_";
-    public static final String DEFAULT_MAP_ITEM_LABEL = "_|->_";
     public static final String DEFAULT_MAP_UNIT_LABEL = ".Map";
-    public static final String DEFAULT_SET_LABEL = "_Set_";
-    public static final String DEFAULT_SET_ITEM_LABEL = "SetItem";
-    public static final String DEFAULT_SET_UNIT_LABEL = ".Set";
 
     /** Name of this data structure sort. */
     private final String name;
diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java
index ba7d513aa0..d1df43bbeb 100644
--- a/kernel/src/main/java/org/kframework/kompile/Kompile.java
+++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java
@@ -20,7 +20,9 @@
 import org.kframework.frontend.KApply;
 import org.kframework.frontend.KORE;
 import org.kframework.frontend.KSequence;
+import org.kframework.frontend.KVariable;
 import org.kframework.frontend.Sort;
+import org.kframework.frontend.SortedADT;
 import org.kframework.frontend.TransformK;
 import org.kframework.frontend.compile.AddImplicitComputationCell;
 import org.kframework.frontend.compile.ConcretizeCells;
@@ -148,7 +150,10 @@ public static Function<Definition, Definition> defaultSteps(KompileOptions kompi
             d = new ResolveAnonVar().apply(d);
             d = new ConvertContextsToHeatCoolRules(kompileOptions).resolve(d);
             d = new ResolveHeatCoolAttribute(new HashSet<>(kompileOptions.transition)).apply(d);
-            d = new ResolveSemanticCasts(kompileOptions.backend.equals(Backends.JAVA)).apply(d);
+            d = new ResolveSemanticCasts(
+                    kompileOptions.backend.equals(Backends.JAVA)
+                            || kompileOptions.backend.equals(Backends.SKALA)
+            ).apply(d);
             d = DefinitionTransformer.fromWithInputDefinitionTransformerClass(GenerateSortPredicateSyntax.class).apply(d);
             d = resolveFreshConstants(d);
             d = AddImplicitComputationCell.transformDefinition(d);
@@ -211,7 +216,7 @@ public static Definition resolveFreshConstants(Definition input) {
 
     public Rule compileRule(CompiledDefinition compiledDef, Rule parsedRule) {
         return (Rule) asScalaFunc((Sentence s) -> new ResolveAnonVar().process(s))
-                .andThen((Sentence s) ->  new ResolveSemanticCasts(kompileOptions.backend.equals(Backends.JAVA)).process(s))
+                .andThen((Sentence s) -> new ResolveSemanticCasts(kompileOptions.backend.equals(Backends.JAVA)).process(s))
                 .andThen(s -> concretizeSentence(s, compiledDef.kompiledDefinition))
                 .apply(parsedRule);
     }
@@ -247,7 +252,7 @@ public K apply(KApply kk) {
             }.apply(k), "Module-qualify sort predicates");
 
     /**
-     * In the Java backend, {@link KSequence}s are treated like {@link KApply}s, so tranform them.
+     * In all our current backends, {@link KSequence}s are treated like {@link KApply}s, so tranform them.
      */
     public static K convertKSeqToKApply(K ruleBody) {
         return new TransformK() {
@@ -256,4 +261,15 @@ public K apply(KSequence kseq) {
             }
         }.apply(ruleBody);
     }
+
+    /**
+     * The Java backend expects sorted variables, so transform them to the sorted flavor.
+     */
+    public static K ADTKVariableToSortedVariable(K ruleBody) {
+        return new TransformK() {
+            public K apply(KVariable kvar) {
+                return new SortedADT.SortedKVariable(kvar.name(), kvar.att());
+            }
+        }.apply(ruleBody);
+    }
 }
diff --git a/kernel/src/main/java/org/kframework/ktest/CmdArgs/KTestOptions.java b/kernel/src/main/java/org/kframework/ktest/CmdArgs/KTestOptions.java
index 058ae94951..e51cfbb052 100644
--- a/kernel/src/main/java/org/kframework/ktest/CmdArgs/KTestOptions.java
+++ b/kernel/src/main/java/org/kframework/ktest/CmdArgs/KTestOptions.java
@@ -145,7 +145,7 @@ public Class<KTestStep> enumClass() {
      * Timeout for processes spawned by ktest. (in seconds)
      */
     @Parameter(names="--timeout", description="Time limit for each process (milliseconds).")
-    private int timeout = 900000;
+    private int timeout = 600000;
 
     /**
      * Update existing .out files.
diff --git a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java b/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java
index 49a1ba41f0..05c3eaeb2b 100644
--- a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java
+++ b/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java
@@ -79,7 +79,8 @@ public static KompileMetaInfo kompilemetaInfo(FileUtil files){
     // NOTE: should be matched with org.kframework.kompile.KompileFrontEnd.save()
     public static CompiledDefinition koreDefinition(BinaryLoader loader, FileUtil files) {
         // org.kframework.definition.Definition kompiledDefinition = loader.loadOrDie(org.kframework.definition.Definition.class, files.resolveKompiled(FileUtil.KOMPILED_DEFINITION_BIN)); // deprecated
-        org.kframework.definition.Definition kompiledDefinition = MiniToKore.apply(parseKore(files));
+        org.kframework.kore.Definition koreDefition = parseKore(files);
+        org.kframework.definition.Definition kompiledDefinition = MiniToKore.apply(koreDefition);
         KompileOptions kompileOptions = loader.loadOrDie(KompileOptions.class, files.resolveKompiled(FileUtil.KOMPILE_OPTIONS_BIN));
         org.kframework.definition.Definition parsedDefinition = loader.loadOrDie(org.kframework.definition.Definition.class, files.resolveKompiled(FileUtil.PARSED_DEFINITION_BIN));
         org.kframework.frontend.KLabel topCellInitializer = loader.loadOrDie(org.kframework.frontend.KLabel.class, files.resolveKompiled(FileUtil.TOP_CELL_INITIALIZER_BIN));
diff --git a/kernel/src/main/javacc/KoreParser.jj b/kernel/src/main/javacc/KoreParser.jj
index 34521935e7..e075eb6d9f 100644
--- a/kernel/src/main/javacc/KoreParser.jj
+++ b/kernel/src/main/javacc/KoreParser.jj
@@ -77,7 +77,7 @@ TOKEN :
 |	<DOTKLIST: ".::KList" | ".KList">
 |	<TOKENLABEL: "#token">
 |   <KLABELLABEL: "#klabel">
-|   <ID_KLABEL: ["#","a"-"z"](["a"-"z","A"-"Z","0"-"9"])*>
+|   <ID_KLABEL: ["#","a"-"z"](["a"-"z","A"-"Z","0"-"9", "@"])*>
 }
 
 MORE :
diff --git a/kernel/src/main/javacc/Outer.jj b/kernel/src/main/javacc/Outer.jj
index cc6f5e0431..9cdaa77b4b 100644
--- a/kernel/src/main/javacc/Outer.jj
+++ b/kernel/src/main/javacc/Outer.jj
@@ -724,7 +724,7 @@ void Group(StringBuilder sb, int state) : {}
 | "]" { matchedToken.kind = RSQUARE; }
 | "(" { matchedToken.kind = LPAREN; }
 | ")" { matchedToken.kind = RPAREN; }
-| <KEY: ["a"-"z","1"-"9"](["A"-"Z", "a"-"z", "-", "0"-"9"])*("<" (["A"-"Z", "a"-"z", "-", "0"-"9"])+ ">")?>
+| <KEY: ["a"-"z","1"-"9"](["A"-"Z", "a"-"z", "-", "0"-"9", "@"])*("<" (["A"-"Z", "a"-"z", "-", "0"-"9"])+ ">")?>
 }
 
 /** The same as 'Attributes()', but requires that the entire input be
@@ -769,8 +769,9 @@ void Tag(ASTNode node) :
 void TagContent(StringBuilder sb) : {}
 {
 ( <TAG_CONTENT> { sb.append(specialAndImage()); }
+| <STRING> { sb.append(specialAndImage()); }
 | "(" { sb.append(specialAndImage()); }
-  TagContent(sb)
+   TagContent(sb)
   ")" { sb.append(specialAndImage()); }
 )*
 }
diff --git a/kernel/src/test/java/org/kframework/frontend/compile/CloseCellsTest.java b/kernel/src/test/java/org/kframework/frontend/compile/CloseCellsTest.java
index ccd92efaa4..be3308e4f4 100644
--- a/kernel/src/test/java/org/kframework/frontend/compile/CloseCellsTest.java
+++ b/kernel/src/test/java/org/kframework/frontend/compile/CloseCellsTest.java
@@ -10,6 +10,7 @@
 
 import org.junit.Test;
 import org.junit.Assert;
+import org.kframework.kore.implementation;
 import org.kframework.utils.errorsystem.KEMException;
 
 import java.util.Arrays;
@@ -19,8 +20,8 @@
 public class CloseCellsTest {
 
     final SortInfo sortInfo = new SortInfo() {{
-        addOp("Map", "_Map_");
-        addOp("List", "_List_");
+        addOp("Map", "Map@MAP");
+        addOp("List", "List@LIST");
     }};
     final TestConfiguration cfgInfo = new TestConfiguration() {{
         addCell(null, "ThreadCell", "<thread>", Multiplicity.STAR);
@@ -35,8 +36,8 @@ public class CloseCellsTest {
         addLabel("EnvCell", "<env>");
         addLabel("ThreadCell", "<thread>");
         addLabel("ListCell", "<list>");
-        addLabel("Map", "_Map_", true, true, true);
-        addLabel("List", "_List_", true, false, true);
+        addLabel("Map", "Map@MAP", true, true, true);
+        addLabel("List", "List@LIST", true, false, true);
     }};
 
     @Test
@@ -50,7 +51,7 @@ public void testSimpleClosure() {
     @Test
     public void testCloseMap() {
         K term = cell("<env>", true, false, KORE.KApply(KLabel("'_|=>_"), intToToken(1), intToToken(2)));
-        K expected = ccell("<env>", KORE.KApply(KLabel("_Map_"), KORE.KApply(KLabel("'_|=>_"), intToToken(1), intToToken(2)), KVariable("DotVar0")));
+        K expected = ccell("<env>", KORE.KApply(KLabel("Map@MAP"), KORE.KApply(KLabel("'_|=>_"), intToToken(1), intToToken(2)), KVariable("DotVar0")));
         Assert.assertEquals(expected, new CloseCells(cfgInfo, sortInfo, labelInfo).close(term));
     }
 
diff --git a/pom.xml b/pom.xml
index 14323c9594..20062ac65d 100644
--- a/pom.xml
+++ b/pom.xml
@@ -18,7 +18,7 @@
     <module>API</module>
     <module>kdoc</module>
     <module>shell</module>
-    <module>kale-backend</module>
+    <module>skala-backend</module>
   </modules>
 
   <scm>
diff --git a/shell/pom.xml b/shell/pom.xml
index 3bb4bd45a0..40f06de093 100644
--- a/shell/pom.xml
+++ b/shell/pom.xml
@@ -31,7 +31,7 @@
         </dependency>
         <dependency>
             <groupId>org.kframework.k</groupId>
-            <artifactId>kale-backend</artifactId>
+            <artifactId>skala-backend</artifactId>
             <version>${project.version}</version>
         </dependency>
         <dependency>
diff --git a/shell/src/main/java/org/kframework/main/Main.java b/shell/src/main/java/org/kframework/main/Main.java
index 173603bc86..fb0b00a3a6 100644
--- a/shell/src/main/java/org/kframework/main/Main.java
+++ b/shell/src/main/java/org/kframework/main/Main.java
@@ -15,8 +15,9 @@
 import org.kframework.backend.java.symbolic.ProofExecutionMode;
 import org.kframework.definition.Module;
 import org.kframework.definition.ProcessedDefinition;
-import org.kframework.kale.KaleBackend;
-import org.kframework.kale.KaleRewriter;
+import org.kframework.backend.skala.SkalaKompile;
+//import KaleRewriter;
+import org.kframework.backend.skala.SkalaRewriter;
 import org.kframework.kast.KastFrontEnd;
 import org.kframework.kast.KastOptions;
 import org.kframework.kdep.KDepFrontEnd;
@@ -122,8 +123,8 @@ public static int runApplication(String toolName, String[] args, File workingDir
             Backend koreBackend;
             if (kompileOptions.backend.equals(Backends.JAVA)) {
                 koreBackend = new JavaBackend(kem, files, kompileOptions.global, kompileOptions);
-            } else if (kompileOptions.backend.equals(Backends.KALE)) {
-                koreBackend = new KaleBackend(kompileOptions, kem);
+            } else if (kompileOptions.backend.equals(Backends.SKALA)) {
+                koreBackend = new SkalaKompile(kompileOptions, kem);
             } else
                 throw new AssertionError("Backend not hooked to the shell.");
             KompileFrontEnd frontEnd = new KompileFrontEnd(kompileOptions, koreBackend, sw, kem, loader, files);
@@ -239,9 +240,9 @@ public static int runApplication(String toolName, String[] args, File workingDir
                 intializeMiniKoreRewriter = new InitializeRewriter(fs, javaExecutionOptions.deterministicFunctions,
                         kRunOptions.global, kem, kRunOptions.experimental.smt, hookProvider, kompileOptions.transition,
                         kRunOptions, files, initializeDefinition);
-            } else if (kompileOptions.backend.equals(Backends.KALE)) {
-                initializeRewriter = KaleRewriter::apply;
-                intializeMiniKoreRewriter = null;
+            } else if (kompileOptions.backend.equals(Backends.SKALA)) {
+                initializeRewriter = null;
+                intializeMiniKoreRewriter = (x -> new SkalaRewriter(x.getKey(), x.getRight()));
             } else {
                 throw new AssertionError("Backend not hooked to the shell.");
             }
diff --git a/kale-backend/pom.xml b/skala-backend/pom.xml
similarity index 91%
rename from kale-backend/pom.xml
rename to skala-backend/pom.xml
index 340c6895e0..016e2749a9 100644
--- a/kale-backend/pom.xml
+++ b/skala-backend/pom.xml
@@ -9,10 +9,10 @@
     <version>4.0.1-SNAPSHOT</version>
     <relativePath>../pom.xml</relativePath>
   </parent>
-  <artifactId>kale-backend</artifactId>
+  <artifactId>skala-backend</artifactId>
   <packaging>jar</packaging>
 
-  <name>K Framework Kale Backend</name>
+  <name>K Framework Skala Backend</name>
 
   <dependencies>
     <dependency>
@@ -21,9 +21,9 @@
       <version>${project.version}</version>
     </dependency>
     <dependency>
-      <groupId>org.kframework.kale</groupId>
+      <groupId>org.kframework</groupId>
       <artifactId>kale_2.12</artifactId>
-      <version>0.4-SNAPSHOT</version>
+      <version>0.6-SNAPSHOT</version>
     </dependency>
   </dependencies>
 
diff --git a/kale-backend/src/main/resources/META-INF/services/org.kframework.main.KModule b/skala-backend/src/main/resources/META-INF/services/org.kframework.main.KModule
similarity index 100%
rename from kale-backend/src/main/resources/META-INF/services/org.kframework.main.KModule
rename to skala-backend/src/main/resources/META-INF/services/org.kframework.main.KModule
diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleBackend.scala b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala
similarity index 62%
rename from kale-backend/src/main/scala/org/kframework/kale/KaleBackend.scala
rename to skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala
index 3132d2aa0e..13505bec8c 100644
--- a/kale-backend/src/main/scala/org/kframework/kale/KaleBackend.scala
+++ b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala
@@ -1,15 +1,17 @@
-package org.kframework.kale
+package org.kframework.backend.skala
 
 import java.util.function.Function
 
+import org.kframework.attributes.Att
 import org.kframework.compile.{AddBottomSortForListsWithIdenticalLabels, NormalizeKSeq}
-import org.kframework.definition.{Definition, DefinitionTransformer}
+import org.kframework.definition.{Definition, DefinitionTransformer, Rule, Sentence}
 import org.kframework.kompile.{CompiledDefinition, Kompile, KompileOptions}
 import org.kframework.frontend.KORE
 import org.kframework.frontend.compile._
+import org.kframework.kore.Rewrite
 import org.kframework.utils.errorsystem.KExceptionManager
 
-class KaleBackend(kompileOptions: KompileOptions, kem: KExceptionManager) extends Backend {
+class SkalaKompile(kompileOptions: KompileOptions, kem: KExceptionManager) extends Backend {
   override def accept(d: CompiledDefinition): Unit = {
     // probably a redundant function
   }
@@ -19,14 +21,12 @@ class KaleBackend(kompileOptions: KompileOptions, kem: KExceptionManager) extend
   def defaultSteps(): Definition => Definition = {
 
     (d => Kompile.defaultSteps(kompileOptions, kem)(d))
-      .andThen(DefinitionTransformer.fromRuleBodyTranformer(RewriteToTop.rewriteToTop, "rewrite to top"))
-      .andThen(DefinitionTransformer.fromSentenceTransformer(new NormalizeAssoc(KORE), "normalize assoc"))
+//      .andThen(DefinitionTransformer.fromRuleBodyTranformer(RewriteToTop.rewriteToTop, "rewrite to top"))
       .andThen(DefinitionTransformer.fromHybrid(AddBottomSortForListsWithIdenticalLabels, "AddBottomSortForListsWithIdenticalLabels"))
       .andThen(Kompile.moduleQualifySortPredicates)
+      .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile.ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable"))
       //      .andThen(new ExpandMacrosDefinitionTransformer(kem, files, globalOptions, kompileOptions))
-      .andThen(DefinitionTransformer.fromSentenceTransformer(new NormalizeAssoc(KORE), "normalize assoc"))
-      //      .andThen(DefinitionTransformer.fromRuleBodyTranformer(ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable"))
       .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile.convertKSeqToKApply, "kseq to kapply"))
-      .andThen(DefinitionTransformer.fromRuleBodyTranformer(NormalizeKSeq, "normalize kseq"))
+    //      .andThen(DefinitionTransformer.fromRuleBodyTranformer(NormalizeKSeq, "normalize kseq"))
   }
 }
diff --git a/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaRewriter.scala b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaRewriter.scala
new file mode 100644
index 0000000000..855ea16d0c
--- /dev/null
+++ b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaRewriter.scala
@@ -0,0 +1,58 @@
+package org.kframework.backend.skala
+
+import java.util.Optional
+
+import org.kframework.definition._
+import org.kframework.frontend._
+import org.kframework.kale.builtin.MapImplementation
+import org.kframework.{RewriterResult, kore}
+import org.kframework.kore.Pattern
+import org.kframework.kore.extended.implicits._
+import org.kframework.minikore.converters.{KoreToMini, MiniToKore}
+import org.kframework.rewriter.SearchType
+
+
+
+class SkalaRewriter(mainModule: Module, koreDefinition: kore.Definition) extends org.kframework.rewriter.Rewriter {
+
+  import org.kframework.kore.implementation.{DefaultBuilders => db}
+
+  val mainKoreModule = koreDefinition.modulesMap(db.ModuleName(mainModule.name))
+
+  val skalaBackend = SkalaBackend(koreDefinition, mainKoreModule)
+
+  val frontendToKore = KoreToMini
+
+  val koreToFrontend = MiniToKore
+
+
+  //Todo: Needed only temporarily until we have pretty printers over Kore.
+  private def filterForPrettyPrinting(p: Pattern): Pattern = p match {
+    case kore.Application(kore.Symbol(".K"), _) => db.Application(KoreToMini.iKSeqNil, Seq())
+    case kore.Application(symbol , args) => db.Application(symbol, args.map(filterForPrettyPrinting))
+    case p:MapImplementation => db.Application(db.Symbol(p.label.name), p.children.map(filterForPrettyPrinting).toSeq)
+    case p@_ => p
+  }
+
+  override def execute(k: K, depth: Optional[Integer]): RewriterResult = {
+    val p: Pattern = frontendToKore(k)
+    var res = p
+    if(depth.isPresent()) {
+      res = skalaBackend.step(p, depth.get)
+    } else {
+      res = skalaBackend.execute(p)
+    }
+
+    new RewriterResult(depth, koreToFrontend(filterForPrettyPrinting(res)))
+  }
+
+  override def `match`(k: K, rule: Rule): K = ???
+
+  override def search(initialConfiguration: K, depth: Optional[Integer], bound: Optional[Integer], pattern: Rule, searchType: SearchType, resultsAsSubstitution: Boolean): K = ???
+
+  override def executeAndMatch(k: K, depth: Optional[Integer], rule: Rule): (RewriterResult, K) = ???
+
+  override def prove(rules: java.util.List[Rule]): java.util.List[K] = ???
+}
+
+
diff --git a/skala-backend/src/test/resources/basic/basic.k b/skala-backend/src/test/resources/basic/basic.k
new file mode 100644
index 0000000000..50c8104ef4
--- /dev/null
+++ b/skala-backend/src/test/resources/basic/basic.k
@@ -0,0 +1,9 @@
+module BASIC-SYNTAX
+    syntax Exp ::= Int
+                   | Exp "+" Exp
+endmodule
+module BASIC
+    imports BASIC-SYNTAX
+    configuration <T> <k> $PGM:Exp </k> </T>
+    rule A:Int + B:Int => A +Int B
+endmodule
\ No newline at end of file
diff --git a/skala-backend/src/test/resources/imp/collatz.imp b/skala-backend/src/test/resources/imp/collatz.imp
new file mode 100644
index 0000000000..860bde549d
--- /dev/null
+++ b/skala-backend/src/test/resources/imp/collatz.imp
@@ -0,0 +1,14 @@
+int m, n, q, r, s;
+m = 10;
+while (!(m<=2)) {
+  n = m;
+  m = m + -1;
+  while (!(n<=1)) {
+    s = s+1;
+    q = n/2;
+    r = q+q+1;
+    if (r<=n) {
+      n = n+n+n+1;
+    } else {n=q;}
+  }
+}
\ No newline at end of file
diff --git a/skala-backend/src/test/resources/imp/imp.k b/skala-backend/src/test/resources/imp/imp.k
new file mode 100644
index 0000000000..cdcfcdcca5
--- /dev/null
+++ b/skala-backend/src/test/resources/imp/imp.k
@@ -0,0 +1,61 @@
+// Copyright (c) 2014-2016 K Team. All Rights Reserved.
+
+module IMP-SYNTAX
+  syntax AExp  ::= Int | Id
+                 | AExp "/" AExp              [left, strict]
+                 > AExp "+" AExp              [left, strict]
+                 | "(" AExp ")"               [bracket]
+  syntax BExp  ::= Bool
+                 | AExp "<=" AExp             [seqstrict, latex({#1}\leq{#2})]
+                 | "!" BExp                   [strict]
+                 > BExp "&&" BExp             [left, strict(1)]
+                 | "(" BExp ")"               [bracket]
+  syntax Block ::= "{" "}"
+                 | "{" Stmt "}"
+  syntax Stmt  ::= Block
+                 | Id "=" AExp ";"            [strict(2)]
+                 | "if" "(" BExp ")"
+                   Block "else" Block         [strict(1)]
+                 | "while" "(" BExp ")" Block
+                 > Stmt Stmt                  [left]
+  syntax Pgm ::= "int" Ids ";" Stmt
+  syntax Ids ::= List{Id,","}
+endmodule
+
+
+module IMP
+  imports IMP-SYNTAX
+  syntax KResult ::= Int | Bool
+
+  configuration <T color="yellow">
+                  <k color="green"> $PGM:Pgm </k>
+                  <state color="red"> .Map </state>
+                </T>
+
+// AExp
+  rule <k> X:Id => I ...</k> <state>... X |-> I ...</state>
+  rule I1 / I2 => I1 /Int I2  requires I2 =/=Int 0
+  rule I1 + I2 => I1 +Int I2
+// BExp
+  rule I1 <= I2 => I1 <=Int I2
+  rule ! T => notBool T
+  rule true && B => B
+  rule false && _ => false
+// Block
+  rule {} => .   [structural]
+  rule {S} => S  [structural]
+// Stmt
+  rule <k> X = I:Int; => . ...</k> <state>... X |-> (_ => I) ...</state>
+  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule if (true)  S else _ => S
+  rule if (false) _ else S => S
+  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+// Pgm
+  rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
+    requires notBool (X in keys(Rho))
+  rule int .Ids; S => S  [structural]
+
+// verification ids
+  syntax Id ::= "n"     [token]
+              | "sum"   [token]
+endmodule
diff --git a/skala-backend/src/test/resources/imp/initialization.imp b/skala-backend/src/test/resources/imp/initialization.imp
new file mode 100644
index 0000000000..8c36cf5e35
--- /dev/null
+++ b/skala-backend/src/test/resources/imp/initialization.imp
@@ -0,0 +1,3 @@
+int a, b;
+a = 1;
+b = 2;
diff --git a/skala-backend/src/test/resources/imp/primes.imp b/skala-backend/src/test/resources/imp/primes.imp
new file mode 100644
index 0000000000..e206f8d8ae
--- /dev/null
+++ b/skala-backend/src/test/resources/imp/primes.imp
@@ -0,0 +1,20 @@
+int i, m, n, q, r, s, t, x, y, z;
+m = 10;  n = 2;
+while (n <= m) {
+  i = 2;  q = n/i;  t = 1;
+  while (i<=q && 1<=t) {
+    x = i;
+    y = q;
+    z = 0;
+    while (!(x <= 0)) {
+      q = x/2;
+      r = q+q+1;
+      if (r <= x) { z = z+y; } else {}
+      x = q;
+      y = y+y;
+    }
+    if (n <= z) { t = 0; } else { i = i+1;  q = n/i; }
+  }
+  if (1 <= t) { s = s+1; } else {}
+  n = n+1;
+}
\ No newline at end of file
diff --git a/skala-backend/src/test/resources/imp/sum.imp b/skala-backend/src/test/resources/imp/sum.imp
new file mode 100644
index 0000000000..69d0df74b8
--- /dev/null
+++ b/skala-backend/src/test/resources/imp/sum.imp
@@ -0,0 +1,8 @@
+int n, sum;
+n = 10;
+sum = 0;
+while (!(n <= 0)) {
+  sum = sum + n;
+  n = n + -1;
+}
+
diff --git a/skala-backend/src/test/resources/imp/sum100.imp b/skala-backend/src/test/resources/imp/sum100.imp
new file mode 100644
index 0000000000..b185eb4564
--- /dev/null
+++ b/skala-backend/src/test/resources/imp/sum100.imp
@@ -0,0 +1,8 @@
+int n, sum;
+n = 100;
+sum = 0;
+while (!(n <= 0)) {
+  sum = sum + n;
+  n = n + -1;
+}
+
diff --git a/skala-backend/src/test/resources/imp/sum1000.imp b/skala-backend/src/test/resources/imp/sum1000.imp
new file mode 100644
index 0000000000..50b73fddcb
--- /dev/null
+++ b/skala-backend/src/test/resources/imp/sum1000.imp
@@ -0,0 +1,8 @@
+int n, sum;
+n = 1000;
+sum = 0;
+while (!(n <= 0)) {
+  sum = sum + n;
+  n = n + -1;
+}
+
diff --git a/k-distribution/src/test/java/org/kframework/frontend/compile/IMPonKale.java b/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java
similarity index 52%
rename from k-distribution/src/test/java/org/kframework/frontend/compile/IMPonKale.java
rename to skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java
index 7cdf23f68f..7ac24cf876 100644
--- a/k-distribution/src/test/java/org/kframework/frontend/compile/IMPonKale.java
+++ b/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java
@@ -1,9 +1,6 @@
-// Copyright (c) 2015-2016 K Team. All Rights Reserved.
-
-package org.kframework.frontend.compile;
+package org.kframework.backend.skala;
 
 import org.junit.Test;
-import org.junit.rules.TestName;
 import org.kframework.attributes.Source;
 import org.kframework.backend.Backends;
 import org.kframework.builtin.Sorts;
@@ -12,80 +9,68 @@
 import org.kframework.frontend.KApply;
 import org.kframework.frontend.KORE;
 import org.kframework.frontend.KToken;
-import org.kframework.kale.KaleBackend;
-import org.kframework.kale.KaleRewriter;
 import org.kframework.kompile.CompiledDefinition;
 import org.kframework.kompile.Kompile;
 import org.kframework.kompile.KompileOptions;
+import org.kframework.kore.Definition;
 import org.kframework.main.GlobalOptions;
-import org.kframework.parser.ProductionReference;
+import org.kframework.minikore.converters.KoreToMini;
 import org.kframework.unparser.AddBrackets;
 import org.kframework.unparser.KOREToTreeNodes;
 import org.kframework.utils.errorsystem.KExceptionManager;
 import org.kframework.utils.file.FileUtil;
 
+import javax.swing.text.html.Option;
 import java.io.File;
-import java.io.IOException;
-import java.net.URISyntaxException;
 import java.util.HashMap;
 import java.util.Map;
 import java.util.Optional;
 import java.util.function.BiFunction;
 
 import static org.junit.Assert.*;
-import static org.kframework.frontend.KORE.*;
-
-public class IMPonKale {
 
-    @org.junit.Rule
-    public TestName name = new TestName();
-
-    protected File testResource(String baseName) throws URISyntaxException {
-        return new File(baseName);
-    }
 
+public class BasicOnSkalaTest {
     @Test
-    public void simple() throws IOException, URISyntaxException {
-        String fileName = "tutorial/1_k/2_imp/lesson_4/imp.k";
-        String program = "int n, sum;\n" +
-                "n = 10;\n" +
-                "sum = 0;\n" +
-                "while (!(n <= 0)) {\n" +
-                "  sum = sum + n;\n" +
-                "  n = n + -1;\n" +
-                "}";
+    public void basicOnSkalaTest1() {
+        String fileName = "src/test/resources/basic/basic.k";
+        String program = "1 + 2";
         Source source = Source.apply("from test");
-        String mainModuleName = "IMP";
+        String mainModuleName = "BASIC";
 
         KExceptionManager kem = new KExceptionManager(new GlobalOptions());
-        File definitionFile = testResource(fileName);
+        File definitionFile = new File(fileName);
         KompileOptions kompileOptions = new KompileOptions();
-        kompileOptions.backend = Backends.KALE;
+        kompileOptions.backend = Backends.SKALA;
         GlobalOptions globalOptions = new GlobalOptions();
         globalOptions.debug = true;
         globalOptions.warnings = GlobalOptions.Warnings.ALL;
 
         Kompile kompile = new Kompile(kompileOptions, FileUtil.testFileUtil(), kem, false);
 
-        CompiledDefinition compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName,  new KaleBackend(kompileOptions, kem).steps());
+        CompiledDefinition compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName, new SkalaKompile(kompileOptions, kem).steps());
 
         BiFunction<String, Source, K> programParser = compiledDef.getProgramParser(kem);
 
         K parsed = programParser.apply(program, source);
 
         Map<KToken, K> map = new HashMap<>();
+
         map.put(KORE.KToken("$PGM", Sorts.KConfigVar()), parsed);
 
-        KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KApply(KLabel("_|->_"), e.getKey(), e.getValue())).reduce(KApply(KLabel(".Map")), (a, b) -> KApply(KLabel("_Map_"), a, b)));
+        KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KORE.KApply(KORE.KLabel("_|->_"), e.getKey(), e.getValue())).reduce(KORE.KApply(KORE.KLabel(".Map")), (a, b) -> KORE.KApply(KORE.KLabel("_Map_"), a, b)));
+
+        Definition definition = KoreToMini.apply(compiledDef.kompiledDefinition);
 
-        KaleRewriter kaleRewriter = new KaleRewriter(compiledDef.executionModule());
+        SkalaRewriter skalaBackendRewriter = new SkalaRewriter(compiledDef.executionModule(), definition);
 
-        K kResult = kaleRewriter.execute(input, Optional.<Integer>empty()).k();
+        K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k();
 
         Module unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule());
 
-        String actual = KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, kResult), unparsingModule)));
+        String actual = KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((org.kframework.parser.ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, kResult), unparsingModule)));
+
+        assertEquals("Execution failed", "<T> <k> 3 </k> </T>", actual);
 
-        assertEquals("Execution failed", "<T> <k> . </k> <state> sum |-> 55 n |-> 0 </state> </T>", actual);
     }
 }
diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java
new file mode 100644
index 0000000000..79900f76fc
--- /dev/null
+++ b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java
@@ -0,0 +1,139 @@
+package org.kframework.backend.skala;
+
+
+import com.sun.tools.javac.util.List;
+import org.junit.AfterClass;
+import org.junit.Before;
+import org.junit.BeforeClass;
+import org.junit.Ignore;
+import org.junit.Test;
+import org.kframework.attributes.Source;
+import org.kframework.backend.Backends;
+import org.kframework.builtin.Sorts;
+import org.kframework.definition.Module;
+import org.kframework.frontend.K;
+import org.kframework.frontend.KApply;
+import org.kframework.frontend.KORE;
+import org.kframework.frontend.KToken;
+import org.kframework.kompile.CompiledDefinition;
+import org.kframework.kompile.Kompile;
+import org.kframework.kompile.KompileOptions;
+import org.kframework.kore.Definition;
+import org.kframework.main.GlobalOptions;
+import org.kframework.minikore.converters.KoreToMini;
+import org.kframework.unparser.AddBrackets;
+import org.kframework.unparser.KOREToTreeNodes;
+import org.kframework.utils.errorsystem.KException;
+import org.kframework.utils.errorsystem.KExceptionManager;
+import org.kframework.utils.file.FileUtil;
+
+import javax.swing.text.html.Option;
+import java.io.File;
+import java.nio.file.Path;
+import java.util.HashMap;
+import java.util.Map;
+import java.util.Optional;
+import java.util.function.BiFunction;
+
+import static org.junit.Assert.assertEquals;
+
+public class ImpOnSkalaTest {
+
+    private static CompiledDefinition compiledDef;
+    private static String resources;
+    private static KExceptionManager kem;
+    private static SkalaRewriter skalaBackendRewriter;
+    private static Module unparsingModule;
+    private static BiFunction<String, Source, K> programParser;
+
+    static long timeBefore = System.nanoTime();
+
+    public static void logTime(String what) {
+        System.out.println(what + ": " + ((System.nanoTime() - timeBefore) / 1000000) + "ms");
+        timeBefore = System.nanoTime();
+    }
+
+    @BeforeClass
+    public static void kompileSetup() {
+        logTime("start");
+        resources = "src/test/resources/imp/";
+        File definitionFile = new File(resources + "imp.k");
+        String mainModuleName = "IMP";
+        KompileOptions kompileOptions = new KompileOptions();
+        kompileOptions.backend = Backends.SKALA;
+        GlobalOptions globalOptions = new GlobalOptions();
+        globalOptions.debug = true;
+        globalOptions.warnings = GlobalOptions.Warnings.ALL;
+        kem = new KExceptionManager(globalOptions);
+        Kompile kompile = new Kompile(kompileOptions, FileUtil.testFileUtil(), kem, false);
+        compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName, new SkalaKompile(kompileOptions, kem).steps());
+        logTime("kompile");
+        Definition definition = KoreToMini.apply(compiledDef.kompiledDefinition);
+        logTime("frontend kore to kore");
+        skalaBackendRewriter = new SkalaRewriter(compiledDef.executionModule(), definition);
+        logTime("make Scala Rewriter");
+        unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule());
+        programParser = compiledDef.getProgramParser(kem);
+        logTime("parse-unparse stuff");
+
+        // warmup
+        K input = getParsedProgram("initialization.imp");
+        K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k();
+        String actual = unparseResult(kResult);
+    }
+
+    private static K getParsedProgram(String pgmName) {
+        String program = FileUtil.load(new File(resources + pgmName));
+        Source source = Source.apply("from test");
+        K parsed = programParser.apply(program, source);
+        Map<KToken, K> map = new HashMap<>();
+        map.put(KORE.KToken("$PGM", Sorts.KConfigVar()), parsed);
+        KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KORE.KApply(KORE.KLabel("_|->_"), KORE.KList(List.of(e.getKey(), e.getValue())))).reduce(KORE.KApply(KORE.KLabel(".Map")), (a, b) -> KORE.KApply(KORE.KLabel("Map@MAP"), a, b)));
+        return input;
+    }
+
+    private static String unparseResult(K result) {
+        return KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((org.kframework.parser.ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, result), unparsingModule)));
+    }
+
+
+    @Test
+    public void sumTest() {
+        K input = getParsedProgram("sum.imp");
+        K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k();
+        String actual = unparseResult(kResult);
+        assertEquals("Execution with Skala Backend Failed", "<T> <k> . </k> <state> 'n |-> 0 'sum |-> 55 </state> </T>", actual);
+    }
+
+    @Test
+    public void sum100Test() {
+        K input = getParsedProgram("sum100.imp");
+        K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k();
+        String actual = unparseResult(kResult);
+        assertEquals("Execution with Skala Backend Failed", "<T> <k> . </k> <state> 'n |-> 0 'sum |-> 5050 </state> </T>", actual);
+    }
+
+    @Test
+    public void sum1000Test() {
+        K input = getParsedProgram("sum1000.imp");
+        K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k();
+        String actual = unparseResult(kResult);
+        assertEquals("Execution with Skala Backend Failed", "<T> <k> . </k> <state> 'n |-> 0 'sum |-> 500500 </state> </T>", actual);
+    }
+
+    @Test
+    public void collatzTest() {
+        K input = getParsedProgram("collatz.imp");
+        K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k();
+        String actual = unparseResult(kResult);
+        assertEquals("Execution with Skala Backend Failed", "<T> <k> . </k> <state> 'n |-> 1 'r |-> 3 'q |-> 1 's |-> 66 'm |-> 2 </state> </T>", actual);
+    }
+
+    @Test
+    public void primesTest() {
+        K input = getParsedProgram("primes.imp");
+        K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k();
+        String actual = unparseResult(kResult);
+        assertEquals("Execution with Skala Backend Failed", "<T> <k> . </k> <state> 'n |-> 11 't |-> 0 'y |-> 20 'x |-> 0 'z |-> 10 'r |-> 1 'q |-> 0 'i |-> 2 's |-> 4 'm |-> 10 </state> </T>", actual);
+    }
+}
diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/PlutusOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/PlutusOnSkalaTest.java
new file mode 100644
index 0000000000..20e9ed9e2d
--- /dev/null
+++ b/skala-backend/src/test/scala/org/kframework/backend/skala/PlutusOnSkalaTest.java
@@ -0,0 +1,91 @@
+package org.kframework.backend.skala;
+
+
+import org.junit.BeforeClass;
+import org.junit.Test;
+import org.kframework.attributes.Source;
+import org.kframework.backend.Backends;
+import org.kframework.builtin.Sorts;
+import org.kframework.definition.Module;
+import org.kframework.frontend.K;
+import org.kframework.frontend.KApply;
+import org.kframework.frontend.KORE;
+import org.kframework.frontend.KToken;
+import org.kframework.kompile.CompiledDefinition;
+import org.kframework.kompile.Kompile;
+import org.kframework.kompile.KompileOptions;
+import org.kframework.kore.Definition;
+import org.kframework.main.GlobalOptions;
+import org.kframework.minikore.converters.KoreToMini;
+import org.kframework.unparser.AddBrackets;
+import org.kframework.unparser.KOREToTreeNodes;
+import org.kframework.utils.errorsystem.KExceptionManager;
+import org.kframework.utils.file.FileUtil;
+
+import java.io.File;
+import java.util.HashMap;
+import java.util.Map;
+import java.util.Optional;
+import java.util.function.BiFunction;
+
+import static org.junit.Assert.*;
+
+public class PlutusOnSkalaTest {
+
+    private static CompiledDefinition compiledDef;
+    private static String resources;
+    private static KExceptionManager kem;
+    private static SkalaRewriter skalaBackendRewriter;
+    private static Module unparsingModule;
+    private static BiFunction<String, Source, K> programParser;
+
+    static long timeBefore = System.nanoTime();
+
+    public static void logTime(String what) {
+        System.out.println(what + ": " + ((System.nanoTime() - timeBefore) / 1000000) + "ms");
+        timeBefore = System.nanoTime();
+    }
+
+    @BeforeClass
+    public static void kompileSetup() {
+        logTime("start");
+        resources = "src/test/resources/plutus/";
+        File definitionFile = new File(resources + "plutus-core.k");
+        String mainModuleName = "PLUTUS-CORE";
+        KompileOptions kompileOptions = new KompileOptions();
+        kompileOptions.backend = Backends.SKALA;
+        GlobalOptions globalOptions = new GlobalOptions();
+        globalOptions.debug = true;
+        globalOptions.warnings = GlobalOptions.Warnings.ALL;
+        kem = new KExceptionManager(globalOptions);
+        Kompile kompile = new Kompile(kompileOptions, FileUtil.testFileUtil(), kem, false);
+        compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName, new SkalaKompile(kompileOptions, kem).steps());
+        logTime("kompile");
+        Definition definition = KoreToMini.apply(compiledDef.kompiledDefinition);
+        logTime("frontend kore to kore");
+        skalaBackendRewriter = new SkalaRewriter(compiledDef.executionModule(), definition);
+        logTime("make Scala Rewriter");
+        unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule());
+        programParser = compiledDef.getProgramParser(kem);
+        logTime("parse-unparse stuff");
+
+        // warmup
+        K input = getParsedProgram("empty.plcore");
+        K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k();
+        String actual = unparseResult(kResult);
+    }
+
+    private static K getParsedProgram(String pgmName) {
+        String program = FileUtil.load(new File(resources + pgmName));
+        Source source = Source.apply("from test");
+        K parsed = programParser.apply(program, source);
+        Map<KToken, K> map = new HashMap<>();
+        map.put(KORE.KToken("$PGM", Sorts.KConfigVar()), parsed);
+        KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KORE.KApply(KORE.KLabel("_|->_"), KORE.KList(e.getKey(), e.getValue()))).reduce(KORE.KApply(KORE.KLabel(".Map")), (a, b) -> KORE.KApply(KORE.KLabel("_Map_"), a, b)));
+        return input;
+    }
+
+    private static String unparseResult(K result) {
+        return KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((org.kframework.parser.ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, result), unparsingModule)));
+    }
+}