diff --git a/tests/plugin/kawaguchi/InsertSort.scala b/tests/plugin/kawaguchi/InsertSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bdd321cb4f66e03b7ba66363f37f952de8f5821e
--- /dev/null
+++ b/tests/plugin/kawaguchi/InsertSort.scala
@@ -0,0 +1,39 @@
+package plugin.kawaguchi
+
+/* Example from paper "Type-based Data Structure Verification"
+ * http://pho.ucsd.edu/liquid/demo/index2.php */
+
+import funcheck.lib.Specs._
+
+object InsertSort {
+
+  def insert(ys: List[Int], x: Int): List[Int] = ys match {
+    case Nil => List(x)
+    case y :: ys => 
+      if (x < y) x :: y :: ys
+      else y :: insert(ys,x)
+  }
+  
+  def insert_sort(xs: List[Int]): List[Int] = xs match {
+    case Nil => Nil
+    case x :: xs => 
+      insert(insert_sort(xs),x)
+  }
+  
+  def insert_sort2(xs: List[Int]): List[Int] = 
+    xs.foldLeft[List[Int]](Nil)((x,xs) => insert(x,xs))
+  
+  def check(xs: List[Int]): Boolean = xs match {
+    case Nil => true
+    case List(x) => true
+    case x :: y :: xs => 
+      x <= y && check(y :: xs)
+  }
+  
+  def test(xs: List[Int]): Boolean = 
+    check(insert_sort(xs)) && check(insert_sort2(xs))
+  
+  forAll{xs: List[Int] => test(xs)}
+  
+  def main(args: Array[String]) = {}
+}