diff --git a/library/lazy/package.scala b/library/lazy/package.scala
index 3d03565d5191ce1d9bf5187100d97166d5b5c782..f329b589abb38457cd8f53e1ebe15209c311f201 100644
--- a/library/lazy/package.scala
+++ b/library/lazy/package.scala
@@ -50,13 +50,13 @@ object $ {
   @inline
   implicit def toWithState[T](x: T) = new WithState(x)
 
-   @library
+  /* @library
   case class Mem[T](v: T) {
     @extern
     def isCached: Boolean = sys.error("not implemented!")
   }
   @inline
-  implicit def toMem[T](x: T) = new Mem(x)
+  implicit def toMem[T](x: T) = new Mem(x)*/
 
   /**
    * annotations for monotonicity proofs.
@@ -88,3 +88,51 @@ case class $[T](f: Unit => T) {
   @extern
   def isSuspension[T](f: T) : Boolean = sys.error("isSuspensionOf method is not executable")
 }
+
+/**
+ * The following are set of methods meant for `Memoized` closures
+ */
+@library
+object Mem {
+  @inline
+  implicit def toMem[T](x: T) = new Mem(x)
+
+  /**
+   * accessing in and out states of mems
+   * Should be used only in ensuring.
+   * TODO: enforce this.
+   */
+  @extern
+  def inState[T] : Set[Mem[T]] = sys.error("inState method is not executable!")
+
+  @extern
+  def outState[T] : Set[Mem[T]] = sys.error("outState method is not executable")
+
+  /**
+   * Helper class for invoking with a given state instead of the implicit state
+   */
+  @library
+  case class memWithState[T](v: T) {
+    @extern
+    def withState[U](u: Set[Mem[U]]): T = sys.error("withState method is not executable!")
+
+    @extern
+    def withState[U, V](u: Set[Mem[U]], v: Set[Mem[V]]): T = sys.error("withState method is not executable!")
+
+    @extern
+    def withState[U, V, W](u: Set[Mem[U]], v: Set[Mem[V]], w: Set[Mem[W]]): T = sys.error("withState method is not executable!")
+
+    @extern
+    def withState[U, V, W, X](u: Set[Mem[U]], v: Set[Mem[V]], w: Set[Mem[W]], x: Set[Mem[X]]): T = sys.error("withState method is not executable!")
+    // extend this to more arguments if needed
+  }
+
+  @inline
+  implicit def toWithState[T](x: T) = new memWithState(x)
+}
+
+@library
+case class Mem[T](v: T) {
+  @extern
+  def isCached: Boolean = sys.error("not implemented!")
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/laziness/LazinessUtil.scala b/src/main/scala/leon/laziness/LazinessUtil.scala
index 1c543fa2dc30791d07c7858d145d813fc8fb4eac..d8a06ac01fc767bf45499f1d1eba482d50b777ce 100644
--- a/src/main/scala/leon/laziness/LazinessUtil.scala
+++ b/src/main/scala/leon/laziness/LazinessUtil.scala
@@ -83,14 +83,16 @@ object LazinessUtil {
 
   def isInStateCall(e: Expr)(implicit p: Program): Boolean = e match {
     case FunctionInvocation(TypedFunDef(fd, _), Seq()) =>
-      fullName(fd)(p) == "leon.lazyeval.$.inState"
+      val fn = fullName(fd)(p)
+      (fn == "leon.lazyeval.$.inState" || fn == "leon.lazyeval.Mem.inState")
     case _ =>
       false
   }
 
   def isOutStateCall(e: Expr)(implicit p: Program): Boolean = e match {
     case FunctionInvocation(TypedFunDef(fd, _), Seq()) =>
-      fullName(fd)(p) == "leon.lazyeval.$.outState"
+      val fn = fullName(fd)(p)
+      (fn == "leon.lazyeval.$.outState" || fn == "leon.lazyeval.Mem.outState")
     case _ =>
       false
   }
@@ -109,13 +111,14 @@ object LazinessUtil {
 
   def isWithStateCons(e: Expr)(implicit p: Program): Boolean = e match {
     case CaseClass(cct, Seq(_)) =>
-      fullName(cct.classDef)(p) == "leon.lazyeval.$.WithState"
+      val fn = fullName(cct.classDef)(p)
+      (fn == "leon.lazyeval.$.WithState" || fn == "leon.lazyeval.Mem.memWithState")
     case _ => false
   }
 
   def isMemCons(e: Expr)(implicit p: Program): Boolean = e match {
     case CaseClass(cct, Seq(_)) =>
-      fullName(cct.classDef)(p) == "leon.lazyeval.$.Mem"
+      fullName(cct.classDef)(p) == "leon.lazyeval.Mem"
     case _ => false
   }
 
@@ -125,7 +128,9 @@ object LazinessUtil {
    */
   def isWithStateFun(e: Expr)(implicit p: Program): Boolean = e match {
     case FunctionInvocation(TypedFunDef(fd, _), _) =>
-      fullName(fd)(p) == "leon.lazyeval.WithState.withState"
+      val fn = fullName(fd)(p)
+      (fn == "leon.lazyeval.WithState.withState" ||
+          fn == "leon.lazyeval.memWithState.withState")
     case _ => false
   }
 
@@ -153,11 +158,17 @@ object LazinessUtil {
     case _ => false
   }
 
+  def isMemType(tpe: TypeTree): Boolean = tpe match {
+    case CaseClassType(CaseClassDef(cid, _, None, false), Seq(_)) =>
+      cid.name == "Mem"
+    case _ => false
+  }
+
   /**
-   * TODO: Check that lazy types are not nested
+   * Lazy types are not nested by precondition
    */
   def unwrapLazyType(tpe: TypeTree) = tpe match {
-    case ctype @ CaseClassType(_, Seq(innerType)) if isLazyType(ctype) =>
+    case ctype @ CaseClassType(_, Seq(innerType)) if isLazyType(ctype) || isMemType(ctype) =>
       Some(innerType)
     case _ => None
   }
diff --git a/src/main/scala/leon/laziness/LazyClosureConverter.scala b/src/main/scala/leon/laziness/LazyClosureConverter.scala
index 45534d6b6a6a9cb60bb1dc1392cbca2c634cb3f8..c587a330283e3899edb77937ff729420c6be3803 100644
--- a/src/main/scala/leon/laziness/LazyClosureConverter.scala
+++ b/src/main/scala/leon/laziness/LazyClosureConverter.scala
@@ -359,9 +359,7 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
       mapNAryOperator(args, op)
 
     case finv @ FunctionInvocation(_, args) if isCachedInv(finv)(p) => // isCached function ?
-      val baseType = args(0).getType match {
-        case cct: CaseClassType => cct.fieldsTypes(0)
-      }
+      val baseType = unwrapLazyType(args(0).getType).get
       val op = (nargs: Seq[Expr]) => ((stOpt: Option[Expr]) => {
         val narg = nargs(0) // there must be only one argument here
         //println("narg: "+narg+" type: "+narg.getType)
diff --git a/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala b/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala
index 6e614db987f43f117eec20705eab8edd67bf5389..419e4c8e12f5d8c101a61be9dbef0a8b945b9d91 100644
--- a/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala
+++ b/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala
@@ -1,5 +1,5 @@
 import leon.lazyeval._
-import leon.lazyeval.$._
+import leon.lazyeval.Mem._
 import leon.lang._
 import leon.annotation._
 import leon.instrumentation._
diff --git a/testcases/lazy-datastructures/memoization/Knapsack.scala b/testcases/lazy-datastructures/memoization/Knapsack.scala
index f896efafb838672b7a065995827e32f4bec4e285..9d8a01b384e938ea819b58f4e504bbbe1690168d 100644
--- a/testcases/lazy-datastructures/memoization/Knapsack.scala
+++ b/testcases/lazy-datastructures/memoization/Knapsack.scala
@@ -1,5 +1,5 @@
 import leon.lazyeval._
-import leon.lazyeval.$._
+import leon.lazyeval.Mem._
 import leon.lang._
 import leon.annotation._
 import leon.instrumentation._
@@ -27,7 +27,7 @@ object Knapscak {
   }
 
   @traceInduct
-  def depsEvalMono(i: BigInt, items: IList, st1: Set[$[BigInt]], st2: Set[$[BigInt]]) = {
+  def depsEvalMono(i: BigInt, items: IList, st1: Set[Mem[BigInt]], st2: Set[Mem[BigInt]]) = {
     require(i >= 0)
     (st1.subsetOf(st2) && (depsEval(i, items) withState st1)) ==> (depsEval(i, items) withState st2)
   } holds
@@ -75,8 +75,8 @@ object Knapscak {
     require(i == 0 || (i > 0 && depsEval(i - 1, items)))
     knapSack(i, items)
   } ensuring (res => {
-    val in = $.inState[BigInt]
-    val out = $.outState[BigInt]
+    val in = Mem.inState[BigInt]
+    val out = Mem.outState[BigInt]
     depsEvalMono(i - 1, items, in, out) &&
       depsEval(i - 1, items) &&
       time <= 40*items.size + 40
diff --git a/testcases/lazy-datastructures/memoization/PackratParsing.scala b/testcases/lazy-datastructures/memoization/PackratParsing.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b25a58ddcafc3c1118eab9498148c66fb9742830
--- /dev/null
+++ b/testcases/lazy-datastructures/memoization/PackratParsing.scala
@@ -0,0 +1,169 @@
+import leon.lazyeval._
+import leon.lazyeval.Mem._
+import leon.lang._
+import leon.annotation._
+import leon.instrumentation._
+//import leon.invariant._
+
+object PackratParsing {
+
+  // same grammar used by Bran Ford ICFP'02 paper.
+  // The code is as unoptimized as it was presented in the paper to mimic a auto-genrated code
+
+  sealed abstract class Terminal
+  case class Open() extends Terminal
+  case class Close() extends Terminal
+  case class Plus() extends Terminal
+  case class Times() extends Terminal
+  case class Digit() extends Terminal
+
+  /*sealed abstract class List {
+    def size: BigInt = {
+      this match {
+        case Cons(_, tail) => 1 + tail.size
+        case Nil() => BigInt(0)
+      }
+    } ensuring(_ >= 0)
+  }
+  case class Cons(x: Terminal, tail: List) extends List // list of terminals
+  case class Nil() extends List*/
+
+  sealed abstract class Result
+  case class Parsed(rest: BigInt) extends Result
+  case class NoParse() extends Result
+
+  /**
+   * A placeholder function for now.
+   */
+  def lookup(i: BigInt): Terminal = {
+    if(i <= -100) Open()
+    else if(i <= 0) Close()
+    else if(i <= 100) Plus()
+    else if(i <= 200) Times()
+    else Digit()
+  }
+
+  @invstate
+  @memoize
+  def pAdd(i: BigInt): Result = {
+    require((i == 0 || (i > 0 && depsEval(i-1))) &&
+        pMul(i).isCached && pPrim(i).isCached &&
+      // lemma inst
+      (pMul(i) match {
+        case Parsed(j) =>
+         if(j >= 0) depsLem(j, i - 1)
+          else true
+        case _ => true
+      }))
+    // Rule 1: Add <- Mul + Add
+    pMul(i) match {
+      case Parsed(j) =>
+        if (j > 0 && lookup(j) == Plus()) {
+          pAdd(j - 1) match {
+            case Parsed(rem) =>
+              Parsed(rem)
+            case _ =>
+              pMul(i) // Rule2: Add <- Mul
+          }
+        } else pMul(i)
+      case _ =>
+        pMul(i)
+    }
+  } ensuring (res => (res match {
+    case Parsed(rem) => rem < i
+    case _           => true
+  }))
+
+  @invstate
+  @memoize
+  def pMul(i: BigInt): Result = {
+    require((i == 0 || (i > 0 && depsEval(i - 1))) && pPrim(i).isCached &&
+      // lemma inst
+      (pPrim(i) match {
+        case Parsed(j) =>
+          if(j>=0) depsLem(j, i - 1)
+          else true
+        case _ => true
+      }))
+    // Rule 1: Mul <- Prim *  Mul
+    pPrim(i) match {
+      case Parsed(j) =>
+        if (j > 0 && lookup(j) == Plus()) {
+          pMul(j - 1) match {
+            case Parsed(rem) =>
+              Parsed(rem)
+            case _ =>
+              pPrim(i) // Rule2: Mul <- Prim
+          }
+        } else pPrim(i)
+      case _ =>
+        pPrim(i)
+    }
+  } ensuring (res => (res match {
+    case Parsed(rem) => rem < i
+    case _           => true
+  }))
+
+  @invstate
+  @memoize
+  def pPrim(i: BigInt): Result = {
+    require(i == 0 || (i > 0 && depsEval(i-1)))
+    val char = lookup(i)
+    if (char == Digit()) {
+      if (i > 0)
+        Parsed(i - 1) // Rule1: Prim <- Digit
+      else
+        Parsed(-1)  // here, we can use bot to convery that the suffix is empty
+    } else if (char == Open() && i > 0) {
+      pAdd(i - 1) match { // Rule 2: pPrim <- ( Add )
+        case Parsed(rem) =>
+          Parsed(rem)
+        case _ =>
+          NoParse()
+      }
+    } else NoParse()
+  } ensuring (res => res match {
+    case Parsed(rem) => rem < i
+    case _           => true
+  })
+
+  def depsEval(i: BigInt): Boolean = {
+    require(i >= 0)
+    (pPrim(i).isCached && pMul(i).isCached && pAdd(i).isCached) &&
+      (if (i == 0) true
+      else depsEval(i - 1))
+  }
+
+  @traceInduct
+  def evalMono(i: BigInt, st1: Set[Mem[Result]], st2: Set[Mem[Result]]) = {
+    require(i >= 0)
+    (st1.subsetOf(st2) && (depsEval(i) withState st1)) ==> (depsEval(i) withState st2)
+  } holds
+
+  @traceInduct
+  def depsLem(x: BigInt, y: BigInt) = {
+    require(x >= 0 && y >= 0)
+    (x <= y && depsEval(y)) ==> depsEval(x)
+  } holds
+
+  def invoke(i: BigInt): (Result, Result, Result) = {
+    require(i == 0 || (i > 0 && depsEval(i-1)))
+    (pPrim(i), pMul(i), pAdd(i))
+  } ensuring (res => {
+    val in = Mem.inState[Result]
+    val out = Mem.outState[Result]
+    (if(i >0) evalMono(i-1, in, out) else true) &&
+    depsEval(i) //&&
+      //time <= 40*items.size + 40
+  })
+
+  def bottomup(i: BigInt): Result = {
+    require(i >= 0)
+    if(i == 0) invoke(i)._3
+    else {
+      val tailres = bottomup(i-1)
+      invoke(i)._3
+    }
+  } ensuring(_ => depsEval(i))
+
+}
diff --git a/testcases/lazy-datastructures/memoization/WeightedScheduling.scala b/testcases/lazy-datastructures/memoization/WeightedScheduling.scala
new file mode 100644
index 0000000000000000000000000000000000000000..838378b26c0f1004c27c02af407ae7b72b8a5d86
--- /dev/null
+++ b/testcases/lazy-datastructures/memoization/WeightedScheduling.scala
@@ -0,0 +1,130 @@
+import leon.lazyeval._
+import leon.lazyeval.Mem._
+import leon.lang._
+import leon.annotation._
+import leon.instrumentation._
+//import leon.invariant._
+
+object WeightedSched {
+  sealed abstract class IList {
+    def size: BigInt = {
+      this match {
+        case Cons(_, tail) => 1 + tail.size
+        case Nil() => BigInt(0)
+      }
+    } ensuring(_ >= 0)
+  }
+  case class Cons(x: (BigInt, BigInt, BigInt), tail: IList) extends IList // a list of pairs of start, finish and weights
+  case class Nil() extends IList
+
+  sealed abstract class LList {
+    def size: BigInt = {
+      this match {
+        case LCons(_, _, tail) => 1 + tail.size
+        case LNil() => BigInt(0)
+      }
+    } ensuring(_ >= 0)
+  }
+  case class LCons(l: IList, pl: LList, tail: LList) extends LList // a list of pointers into IList, and LList
+  case class LNil() extends LList
+
+  @inline
+  def max(x: BigInt, y: BigInt) = if (x >= y) x else y
+
+  def allEval(jobs: IList): Boolean = {
+    optValOfSched(jobs).isCached &&
+      (jobs match {
+        case Nil()         => true
+        case Cons(_, tail) => allEval(tail)
+      })
+  }
+
+  def depsEval(jobs: IList): Boolean = {
+    jobs match {
+      case Nil() => true
+      case Cons(_, tail) => allEval(tail)
+    }
+  }
+
+  @traceInduct
+  def evalMono(jobs: IList, st1: Set[Mem[BigInt]], st2: Set[Mem[BigInt]]) = {
+    (st1.subsetOf(st2) && (allEval(jobs) withState st1)) ==> (allEval(jobs) withState st2)
+  } holds
+
+  @invstate
+  def skip(jobs: IList, finishBound: BigInt): BigInt = {
+    require(allEval(jobs))
+    jobs match {
+      case Nil() => BigInt(0)
+      case Cons((st, fn, v), tail) =>
+        if(fn > finishBound)
+          skip(tail, finishBound) // cannot include this
+          else
+            optValOfSched(jobs)
+    }
+  } //ensuring(_ => time <= 40*currList.size + 20) // interchanging currList and items in the bound will produce a counter-example
+
+  /**
+   * (a) assuming that jobs are sorted in descending order of the finish times
+   * (b) 'prev' - previous compatibility list for each job (assuming it is precomputed)
+   */
+  @memoize
+  def optValOfSched(jobs: IList, prev: LList): BigInt = {
+    //require(depsEval(jobs))
+    (jobs, prev) match {
+      case (Nil(), _) => BigInt(0)
+      case (Cons((st, fn, v), tail), LCons(prevJobs, prevPres, ptail)) =>
+        val tailres = optValOfSched(tail, ptail)
+        // we may either include the head job or not:
+        // if we include the head job, we have to skip every job that overlaps with it
+        max(v + optValOfSched(prevJobs, prevPres), tailres)
+      case _ =>
+        BigInt(0) // these cases should not be reachable
+    }
+  } ensuring(res => {
+    val in = Mem.inState[BigInt]
+    val out = Mem.outState[BigInt]
+    ((depsEval(jobs) withState in) ==> (in == out)) &&
+      depsEval(jobs) &&
+      (jobs match {
+        case Nil() => true
+        case Cons(_, tail) =>
+          evalMono(tail, out, out ++ Set(Mem(optValOfSched(jobs)))) // lemma instantiation
+      })
+  })
+
+  /*def invoke(jobs: IList) = {
+    require(depsEval(jobs))
+    optValOfSched(jobs)
+  } ensuring (res => {
+    val in = $.inState[BigInt]
+    val out = $.outState[BigInt]
+    (jobs match {
+      case Nil() => true
+      case Cons(_, tail) => evalMono(tail, in, out)
+    }) &&
+    allEval(jobs) //&&
+      //time <= 40*items.size + 40
+  })*/
+
+  /*def bottomup(jobs: IList): IList = {
+    jobs match {
+      case Nil() =>
+        Cons((0, 0, invoke(jobs)), Nil())
+      case Cons((st, ft, value), tail) =>
+        val tailres = bottomup(tail)
+        Cons((st, ft, invoke(jobs)), tailres)
+    }
+  } ensuring(_ => allEval(jobs))*/
+    //items.size <= 10 ==> time <= 500 * (w - i + 1))
+
+  /**
+   * Given a list of jobs (with weights) sorted in descending order of their finish times,
+   * computes the value of the optimal scheduling scheduling.
+   */
+  /*def optSols(jobs: IList) = {
+    //require(w >= 0 && items.size <= 10) //  the second requirement is only to keep the bounds linear for z3 to work
+    bottomup(jobs)
+  } //ensuring(time <= 500*w + 510)
+*/
+}