From 3250ff846cf2ea8ea4a2e849f57de4cc5ba71671 Mon Sep 17 00:00:00 2001
From: Casey Klein <clklein@racket-lang.org>
Date: Sat, 29 Jan 2011 15:25:14 -0600
Subject: [PATCH] Adds a Redex version of Jay's continuation mark
 transformation

---
 collects/meta/props                           |   2 +-
 collects/redex/examples/README                |   4 +
 .../examples/cont-mark-transform/CMT-test.rkt | 296 ++++++++++++++
 .../examples/cont-mark-transform/CMT.rkt      | 232 +++++++++++
 .../cont-mark-transform/SL-semantics-test.rkt | 376 ++++++++++++++++++
 .../cont-mark-transform/SL-semantics.rkt      | 126 ++++++
 .../cont-mark-transform/SL-syntax.rkt         |  44 ++
 .../cont-mark-transform/TL-semantics-test.rkt |  21 +
 .../cont-mark-transform/TL-semantics.rkt      |  19 +
 .../cont-mark-transform/TL-syntax.rkt         |  30 ++
 .../examples/cont-mark-transform/all-test.rkt |   5 +
 .../examples/cont-mark-transform/common.rkt   |  78 ++++
 .../cont-mark-transform/randomized-tests.rkt  | 232 +++++++++++
 .../cont-mark-transform/test-util.rkt         |  84 ++++
 collects/redex/tests/run-tests.rkt            |   1 +
 15 files changed, 1549 insertions(+), 1 deletion(-)
 create mode 100644 collects/redex/examples/cont-mark-transform/CMT-test.rkt
 create mode 100644 collects/redex/examples/cont-mark-transform/CMT.rkt
 create mode 100644 collects/redex/examples/cont-mark-transform/SL-semantics-test.rkt
 create mode 100644 collects/redex/examples/cont-mark-transform/SL-semantics.rkt
 create mode 100644 collects/redex/examples/cont-mark-transform/SL-syntax.rkt
 create mode 100644 collects/redex/examples/cont-mark-transform/TL-semantics-test.rkt
 create mode 100644 collects/redex/examples/cont-mark-transform/TL-semantics.rkt
 create mode 100644 collects/redex/examples/cont-mark-transform/TL-syntax.rkt
 create mode 100644 collects/redex/examples/cont-mark-transform/all-test.rkt
 create mode 100644 collects/redex/examples/cont-mark-transform/common.rkt
 create mode 100644 collects/redex/examples/cont-mark-transform/randomized-tests.rkt
 create mode 100644 collects/redex/examples/cont-mark-transform/test-util.rkt

diff --git a/collects/meta/props b/collects/meta/props
index 6ab349f257..6159e50ac2 100755
--- a/collects/meta/props
+++ b/collects/meta/props
@@ -1243,7 +1243,7 @@ path/s is either such a string or a list of them.
 "collects/redex/tests/matcher-test.rkt" drdr:command-line (mzc *)
 "collects/redex/tests/pict-test.rkt" drdr:command-line (mzc *)
 "collects/redex/tests/rg-test.rkt" drdr:command-line (mzc *)
-"collects/redex/tests/run-tests.rkt" drdr:command-line (gracket-text * "--examples" "--no-bitmaps") drdr:timeout 300
+"collects/redex/tests/run-tests.rkt" drdr:command-line (gracket-text * "--examples" "--no-bitmaps") drdr:timeout 360
 "collects/redex/tests/term-test.rkt" drdr:command-line (mzc *)
 "collects/redex/tests/tl-test.rkt" drdr:command-line (mzc *)
 "collects/repo-time-stamp" responsible (eli)
diff --git a/collects/redex/examples/README b/collects/redex/examples/README
index 2a3396e5b0..51232ead99 100644
--- a/collects/redex/examples/README
+++ b/collects/redex/examples/README
@@ -18,6 +18,10 @@ to demonstrate various different uses of PLT Redex:
   closure. Also, one of the first examples from Matthias
   Felleisen and Matthew Flatt's monograph
 
+  cont-mark-transform: the continuation mark transformation from
+  McCarthy's ICFP '09 paper “Automatically RESTful Web Applications
+  Or, Marking Modular Serializable Continuations" 
+
   contracts.rkt: A core contract calculus, including blame, 
   with function contracts, (eager) pair contracts, 
   and a few numeric predicates
diff --git a/collects/redex/examples/cont-mark-transform/CMT-test.rkt b/collects/redex/examples/cont-mark-transform/CMT-test.rkt
new file mode 100644
index 0000000000..0e34d89048
--- /dev/null
+++ b/collects/redex/examples/cont-mark-transform/CMT-test.rkt
@@ -0,0 +1,296 @@
+#lang racket
+
+(require "CMT.rkt"
+         "SL-syntax.rkt"
+         "SL-semantics.rkt"
+         "TL-syntax.rkt"
+         "TL-semantics.rkt"
+         "common.rkt"
+         "test-util.rkt"
+         redex)
+
+(define-syntax (test-translation stx)
+  (syntax-case stx ()
+    [(_ expr)
+     #`(with-handlers ([exn:fail?
+                        (λ (exn)
+                          #,(syntax/loc stx 
+                              (test-equal (exn-message exn) "")))])
+         (let ([e (term expr)])
+           (let ([v ((make-eval -->SL (redex-match SL v))
+                     (term (∅ / ,e)))]
+                 [u ((make-eval -->TL (redex-match TL v))
+                     (term (∅ / (translate ,e))))])
+             #,(syntax/loc stx (test-equal u v)))))]))
+
+(test-translation
+ ((λ (x) ("S" x))
+  (call/cc (λ (k) (k ("Z"))))))
+
+; two marks with the same key on the same frame
+(test-translation
+ ((λ (x) x)
+  (w-c-m ("a") ("1")
+         (w-c-m ("a") ("2")
+                (c-c-m [("a")])))))
+
+; mark reapplied to the reconstituted continuation
+(test-translation
+ (w-c-m ("a") ("1")
+        (w-c-m ("a") ("2")
+               ((λ (x) (x))
+                (call/cc (λ (k) (k (λ () (c-c-m [("a")])))))))))
+
+; variables as keys/values in w-c-ms in context
+(test-translation
+ ((λ (x y z)
+    (w-c-m x y
+           (w-c-m x z
+                  ((λ (x) (x))
+                   (call/cc (λ (k) (k (λ () (c-c-m [x])))))))))
+  ("a") ("1") ("2")))
+
+; transforms a context that includes variables in application frame
+(test-translation
+ ((λ (f)
+    (f (w-c-m ("a") ("1")
+              ((call/cc (λ (k) (k (λ () (c-c-m [("a")])))))))))
+  (λ (x) x)))
+
+; transformation within installed continuation marks
+(test-translation
+ (w-c-m ("a") (λ () (call/cc (λ (k) (k (λ () (c-c-m [("a")]))))))
+        ((λ (frames)
+           (match frames
+             [("cons" cms _)
+              (match cms
+                [("cons" cm _)
+                 (match cm
+                   [("cons" _ t)
+                    ((t))])])]))
+         (c-c-m [("a")]))))
+
+; a continuation, in a values-only position, that contains
+; multiple frames, each with continuation marks
+(test-translation
+ (letrec ([(ref k) (κ ((λ (x) ("outer" x))
+                       (w-c-m ("a") ("1")
+                              (w-c-m ("b") ("2")
+                                     ((λ (x) ("inner" x))
+                                      (w-c-m ("a") ("3")
+                                             (w-c-m ("b") ("4")
+                                                    (hole))))))))])
+   ((λ (x) ("skipped" x))
+    ((ref k) (λ () (c-c-m [("a") ("b")]))))))
+
+; produces a call to map-set where one argument is a (K x).
+(test-translation
+ (λ (x) (w-c-m ("k" x) ("l") (x))))
+
+; application and match translation redexes allow variables
+; in datatype instances
+(test-translation
+ (λ (x) (x ("k" x))))
+(test-translation
+ (λ (x) (match ("k" x) [("k" x) x])))
+
+; w-c-m translation redex with non-w body
+(test-translation
+ (λ (x)
+   (w-c-m ("a") ("b")
+          ("c" x))))
+
+; continuation value in continuation mark of a continuation value
+(test-translation
+ ((λ (x) ("skipped" x))
+  ((κ (w-c-m ("a") (κ ((λ (x) ("wrapped" x)) hole))
+             ((λ (x) ("skipped" x))
+              (hole))))
+   (λ ()
+     ((λ (ms)
+        (match ms
+          [("cons" f _)
+           (match f
+             [("cons" m _)
+              (match m
+                [("cons" _ k)
+                 (k ("a"))])])]))
+      (c-c-m [("a")]))))))
+
+(test-->>
+ -->TL
+ #:cycles-ok
+ (term
+  (∅
+   /
+   (translate
+    ((λ (t) (t t))
+     (call/cc (λ (x) (call/cc x))))))))
+
+(test-translation
+ ((λ (bh)
+    ((λ (x y) ("pair" x y))
+     bh
+     (λ (x) x)))
+  (letrec ([(ref bh) (ref bh)]) (ref bh))))
+
+(test-TL-result
+ (make-store [reverse ,TL-reverse])
+ (,TL-equal? ("1") ("1"))
+ ("true"))
+
+(test-TL-result
+ (make-store [reverse ,TL-reverse])
+ (,TL-equal? ("1") ("2"))
+ ("false"))
+
+(test-TL-result
+ (make-store [reverse ,TL-reverse])
+ (w-c-m ("1") ("whatever") (,TL-equal? ("1") ("1")))
+ ("true"))
+
+(test-TL-result
+ (make-store [equal? ,TL-equal?] [reverse ,TL-reverse] [map-set ,map-set])
+ ((ref map-set) ("nil") ("1") ("a"))
+ ("cons" ("cons" ("1") ("a")) ("nil")))
+
+(test-TL-result
+ (make-store [equal? ,TL-equal?] [reverse ,TL-reverse] [map-set ,map-set])
+ ((ref map-set) ("cons" ("cons" ("1") ("a"))
+                        ("cons" ("cons" ("2") ("b"))
+                                ("nil")))
+                ("2") ("c"))
+ ("cons" ("cons" ("1") ("a"))
+         ("cons" ("cons" ("2") ("c"))
+                 ("nil"))))
+
+(test-TL-result
+ (make-store [c-w-i-c-m ,c-w-i-c-m] [reverse ,TL-reverse])
+ (w-c-m ("a") ("1")
+        ((λ (x) x)
+         ((ref c-w-i-c-m) ("a") (λ (x) x) ("2"))))
+ ("2"))
+
+(test-TL-result
+ (make-store [c-w-i-c-m ,c-w-i-c-m] [reverse ,TL-reverse])
+ (w-c-m ("a") ("1")
+        ((ref c-w-i-c-m) ("a") (λ (x) ("b" x)) ("dontcare")))
+ ("b" ("1")))
+
+(test-TL-result
+ (make-store [restore-marks ,restore-marks])
+ ((ref restore-marks)
+  ("cons" ("cons" ("a") ("1"))
+          ("cons" ("cons" ("b") ("2"))
+                  ("nil")))
+  (λ () (c-c-m [("a") ("b")])))
+ ("cons"
+  ("cons" ("cons" ("b") ("2"))
+          ("cons" ("cons" ("a") ("1"))
+                  ("nil")))
+  ("nil")))
+
+;; Variables and Values
+(test-equal (term (CMT/a z)) (term z))
+(test-equal (term (CMT/a (ref foo))) (term (ref foo)))
+(test-equal (term (CMT/a (λ (x) z))) (term (λ (x) z)))
+
+(define TL-empty-cont
+  (term (λ (x) 
+          (abort 
+           ((ref resume)
+            ("cons"
+             ("cons" ("cons" ("diamond") ("nil"))
+                     ("nil"))
+             ("nil"))
+            x)))))
+(test-equal (term (CMT/a (κ hole))) TL-empty-cont)
+
+(test-equal 
+ (term (CMT/a (κ ((ref f) (ref y) hole))))
+ (term (λ (x1) 
+         (abort
+          ((ref resume)
+           ("cons"
+            ("cons" ("cons" ("diamond") ("nil")) 
+                    ("nil"))
+            ("cons"
+             ("cons" ("cons" ("diamond") ("nil"))
+                     ("cons"
+                      ("cons" ("square") (λ (x) ((ref f) (ref y) x)))
+                      ("nil")))
+             ("nil")))
+           x1)))))
+
+(test-equal (term (CMT/a ("nil"))) (term ("nil")))
+(test-equal (term (CMT/a ("cons" x ("nil")))) (term ("cons" x ("nil"))))
+
+(test-equal 
+ (term (CMT/a ("cons" (κ hole) ("nil"))))
+ (term ("cons" ,TL-empty-cont ("nil"))))
+
+;; Redexes
+(test-equal (term (CMT/r (f x y))) (term (f x y)))
+(test-equal 
+ (term (CMT/r (f x (κ hole)))) 
+ (term (f x ,TL-empty-cont)))
+
+(test-equal (term (CMT/r (letrec ([(ref x) ("nil")]) z))) 
+            (term (letrec ([(ref x) ("nil")]) z)))
+
+(test-equal 
+ (term (CMT/r (letrec ([(ref x) (κ hole)]) 
+                (κ hole))))
+ (term (letrec ([(ref x) ,TL-empty-cont])
+         ,TL-empty-cont)))
+
+(test-equal (term (CMT/r (call/cc f)))
+            (term (f ((ref kont/ms) (c-c-m [("square") ("diamond")])))))
+
+(test-equal (term (CMT/r (match (κ hole) [("nil") (κ hole)]))) 
+            (term (match ,TL-empty-cont
+                    [("nil") ,TL-empty-cont])))
+
+;; Contexts
+(test-equal (term (CMT/T hole)) (term hole))
+
+(test-equal (term (CMT/T ((ref f) (ref y) hole)))
+            (term ((λ (x) ((ref f) (ref y) x))
+                   (w-c-m ("square") (λ (x) ((ref f) (ref y) x))
+                          hole))))
+
+;; Compositions + Whole Programs
+(test-equal
+ (term (CMT ((ref f) (ref y) (call/cc (λ (k) (k z))))))
+ (term
+  ((λ (x) ((ref f) (ref y) x))
+   (w-c-m ("square") (λ (x) ((ref f) (ref y) x))
+          ((λ (k) (k z))
+           ((ref kont/ms) (c-c-m [("square") ("diamond")])))))))
+
+;; Sub-units of big test
+(test-equal (term (CMT ((ref +) ,(num 1) tmp)))
+            (term ((ref +) ,(num 1) tmp)))
+
+;;; Running the resulting programs
+(define (CMT--> sl-version expected-ans)  
+  (define tl-version
+    (term (translate ,sl-version)))
+  (test-TL-result
+   (make-store [= ,=-impl] 
+               [+ ,+-impl]
+               [- ,--impl]
+               [* ,*-impl]
+               [if ,if-impl]) 
+   ,tl-version
+   ,expected-ans))
+
+(CMT--> `(call/cc (λ (k) 
+                    ((λ (tmp) ((ref +) ,(num 2) tmp))
+                     (k ,(num 3)))))
+        (num 3))
+(CMT--> `((λ (tmp) ((ref +) ,(num 1) tmp))
+          (call/cc (λ (k) 
+                     ((λ (tmp) ((ref +) ,(num 2) tmp))
+                      (k ,(num 3))))))
+        (num 4))
\ No newline at end of file
diff --git a/collects/redex/examples/cont-mark-transform/CMT.rkt b/collects/redex/examples/cont-mark-transform/CMT.rkt
new file mode 100644
index 0000000000..6a63795897
--- /dev/null
+++ b/collects/redex/examples/cont-mark-transform/CMT.rkt
@@ -0,0 +1,232 @@
+#lang racket
+
+(require "SL-syntax.rkt"
+         "SL-semantics.rkt"
+         "TL-syntax.rkt"
+         redex)
+
+(provide CMT translate
+         TL-equal? TL-reverse 
+         map-set c-w-i-c-m
+         restore-marks resume
+         CMT/a CMT/r CMT/T)
+
+(define-metafunction SL
+  [(CMT a) (CMT/a a)]
+  [(CMT (in-hole T r))
+   (in-hole (CMT/T T) (CMT/r r))])
+
+(define-metafunction SL
+  [(CMT/a x) x]
+  [(CMT/a σ) σ]
+  [(CMT/a (λ (x ...) e))
+   (λ (x ...) (CMT e))]
+  [(CMT/a (κ E))
+   (λ (x) (abort ((ref resume) v x)))
+   (where v (resume-marks E))
+   (where x ,(variable-not-in (term v) (term x)))]
+  [(CMT/a (K a ...))
+   (K (CMT/a a) ...)])
+
+(define-metafunction SL
+  [(CMT/r (a ...))
+   ((CMT/a a) ...)]
+  [(CMT/r (letrec ([σ w] ...) e))
+   (letrec ([σ (CMT/a w)] ...) (CMT e))]
+  [(CMT/r (w-c-m a ...))
+   (w-c-m (CMT/a a) ...)]
+  [(CMT/r (c-c-m [a ...]))
+   (c-c-m [(CMT/a a) ...])]
+  [(CMT/r (match a l ...))
+   (match (CMT/a a) (CMT/r l) ...)]
+  [(CMT/r [(K x ...) e])
+   [(K x ...) (CMT e)]]
+  [(CMT/r (abort e))
+   (abort (CMT e))]
+  [(CMT/r (call/cc w))
+   ((CMT/a w) ((ref kont/ms) (c-c-m [("square") ("diamond")])))])
+
+(define-metafunction SL
+  [(CMT/T hole) hole]
+  [(CMT/T (a ... T))
+   (v_K (w-c-m ("square") v_K (CMT/T T)))
+   (where (a_* ...) ((CMT/a a) ...))
+   (where x ,(variable-not-in (term (a_* ...)) (term x)))
+   (where v_K (λ (x) (a_* ... x)))]
+  [(CMT/T (w-c-m a_1 a_2 T))
+   (w-c-m a_1* a_2*
+          ((ref c-w-i-c-m)
+           ("diamond")
+           (λ (x_cms)
+             ((λ (x_cms’) 
+                (w-c-m ("diamond") x_cms’ any_T))
+              ((ref map-set) x_cms a_1* a_2*)))
+           ("nil")))
+   (where any_T (CMT/T T)) ; w-c-m case does not produce a T
+   (where a_1* (CMT/a a_1))
+   (where a_2* (CMT/a a_2))
+   (where (x_cms x_cms’) ,(variables-not-in (term (any_T a_1* a_2*)) '(cms cms’)))])
+
+(define-metafunction SL
+  [(resume-marks E) 
+   (resume-marks E #f ("nil"))]
+  
+  [(resume-marks hole k a_m)
+   ("cons" (frame-marks k a_m) ("nil"))]
+  [(resume-marks (w-c-m a_1 a_2 T) k a_m)
+   (resume-marks T k ("cons" ("cons" (CMT a_1) (CMT a_2)) a_m))]
+  [(resume-marks (a ... T) k a_m)
+   ("cons" (frame-marks k a_m)
+           (resume-marks T (λ (x) (a_* ... x)) ("nil")))
+   (where (a_* ...) ((CMT a) ...))
+   (where x ,(variable-not-in (term (a_* ...)) (term x)))])
+
+(define-metafunction SL
+  [(frame-marks #f a_m)
+   ("cons" ("cons" ("diamond") (reverse-marks a_m))
+           ("nil"))]
+  [(frame-marks v_k a_m)
+   ("cons" ("cons" ("diamond") (reverse-marks a_m))
+           ("cons" ("cons" ("square") v_k)
+                   ("nil")))])
+
+(define-metafunction SL
+  [(reverse-marks a)
+   (reverse-marks a ("nil"))]
+  [(reverse-marks ("nil") a) a]
+  [(reverse-marks ("cons" a_1 a_2) a_3)
+   (reverse-marks a_2 ("cons" a_1 a_3))])
+
+(define-metafunction SL
+  translate : e_1 -> (side-condition e_2 (TL-e? (term e_2)))
+  [(translate e)
+   (letrec ([(ref resume) ,resume]
+            [(ref restore-marks) ,restore-marks]
+            [(ref c-w-i-c-m) ,c-w-i-c-m]
+            [(ref map-set) ,map-set]
+            [(ref kont/ms) ,kont/ms]
+            [(ref equal?) ,TL-equal?]
+            [(ref reverse) ,TL-reverse])
+     (CMT e))])
+(define TL-e? (redex-match TL e))
+
+(define kont/ms
+  (term
+   (λ (m)
+     (λ (x)
+       (abort ((ref resume) m x))))))
+
+(define c-w-i-c-m
+  (term
+   (λ (k proc default-v)
+     ((λ (cms)
+        ((λ (reversed)
+           (proc
+            (match reversed
+              [("cons" _ rest)
+               (match rest
+                 [("cons" frame _)
+                  (match frame
+                    [("nil") default-v]
+                    [("cons" mark _)
+                     (match mark
+                       [("cons" _ value) value])])])])))
+         ((ref reverse) cms ("nil"))))
+      (c-c-m [k])))))
+
+(define map-set
+  (term
+   (λ (map k v)
+     (match map
+       [("nil") ("cons" ("cons" k v) ("nil"))]
+       [("cons" pair rest)
+        (match pair
+          [("cons" k’ v’)
+           ((λ (eq)
+              (match eq
+                [("true")
+                 ("cons" ("cons" k v) rest)]
+                [("false")
+                 ((λ (rest’) ("cons" pair rest’))
+                  ((ref map-set) rest k v))]))
+            ((ref equal?) k k’))])]))))
+
+(define restore-marks
+  (term
+   (λ (cms thnk)
+     (match cms
+       [("nil") (thnk)]
+       [("cons" cm cms)
+        (match cm
+          [("cons" m v)
+           (w-c-m m v
+                  ((ref restore-marks) cms thnk))])]))))
+
+(define resume
+  (term
+   (λ (l v)
+     (match l
+       [("nil") v]
+       [("cons" ms l)
+        (match ms
+          [("nil") ((ref resume) l v)]
+          [("cons" m ms)
+           (match m
+             [("cons" j u)
+              (match j
+                [("square")
+                 (match ms 
+                   [("nil") 
+                    (u (w-c-m ("square") u 
+                              ((ref resume) l v)))]
+                   ; How do you get a frame with both marks where square appears first?
+                   ; All frames not introduced by "runtime" calls are marked first with
+                   ; square (thus reported after any diamond mark), and `resume' seems
+                   ; to restore this invariant. Use randomized testing to investigate.
+                   [("cons" cms-mark _)
+                    (match cms-mark
+                      [("cons" _ cms)
+                       (u (w-c-m ("square") u
+                                 ((ref restore-marks) 
+                                  cms
+                                  (λ () 
+                                    (w-c-m ("diamond") cms ((ref resume) l v))))))])])]
+                [("diamond")
+                 (match ms
+                   [("nil")
+                    ((ref restore-marks)
+                     u
+                     (λ () (w-c-m ("diamond") u ((ref resume) l v))))]
+                   [("cons" kont-mark _)
+                    (match kont-mark
+                      [("cons" _ k)
+                       (k (w-c-m ("square") k
+                                 ((ref restore-marks)
+                                  u
+                                  (λ ()
+                                    (w-c-m ("diamond") u ((ref resume) l v))))))])])])])])]))))
+
+(define TL-equal?
+  (term
+   (λ (x y)
+     ((λ (cms)
+        ((λ (reversed)
+           (match reversed
+             [("cons" frame _)
+              (match frame
+                [("cons" _ rest)
+                 (match rest
+                   [("nil") ("true")]
+                   [("cons" _ __) ("false")])])]))
+         ((ref reverse) cms ("nil"))))
+      (w-c-m x ("")
+             (w-c-m y ("")
+                    (c-c-m [x y])))))))
+
+(define TL-reverse
+  (term
+   (λ (xs onto)
+     (match xs
+       [("nil") onto]
+       [("cons" x xs’)
+        ((ref reverse) xs’ ("cons" x onto))]))))
\ No newline at end of file
diff --git a/collects/redex/examples/cont-mark-transform/SL-semantics-test.rkt b/collects/redex/examples/cont-mark-transform/SL-semantics-test.rkt
new file mode 100644
index 0000000000..1d5c8ca05e
--- /dev/null
+++ b/collects/redex/examples/cont-mark-transform/SL-semantics-test.rkt
@@ -0,0 +1,376 @@
+#lang racket
+
+(require "SL-syntax.rkt"
+         "SL-semantics.rkt"
+         "common.rkt"
+         "test-util.rkt"
+         redex)
+
+(test-SL-result
+ ∅ 
+ ((λ (x) ("S" x)) ("Z"))
+ ("S" ("Z")))
+
+(test-SL-stuck ∅ ((λ (x) ("S" x)) ("Z") ("Z")))
+
+(test-SL-result
+ ∅
+ (match ("a" ("1"))
+   [("a" x) x]
+   [("b" y) y])
+ ("1"))
+
+(test-SL-result
+ ∅
+ (match ("b" ("1"))
+   [("a" x) x]
+   [("b" y) y])
+ ("1"))
+
+(test-SL-stuck
+ ∅
+ (match ("a" ("1"))
+   [("a" x) x]
+   [("a" y) y]))
+
+(test-SL-result
+ ∅
+ (letrec ([(ref build-list)
+           (λ (n f)
+             (match n
+               [("Z") ("nil")]
+               [("S" m) 
+                ((λ (x)
+                   ((λ (xs) ("cons" x xs))
+                    ((ref build-list) m f)))
+                 (f m))]))])
+   ((ref build-list) ("S" ("S" ("S" ("Z")))) (λ (i) ("S" i))))
+ ("cons" ("S" ("S" ("S" ("Z"))))
+         ("cons" ("S" ("S" ("Z")))
+               ("cons" ("S" ("Z"))
+                     ("nil")))))
+
+(test-SL-result
+ ∅
+ ((λ (clobber)
+    ((λ (a)
+       ((λ (b) (a))
+        (clobber ("b"))))
+     (clobber ("a"))))
+  (λ (x)
+    (letrec ([(ref y) (λ () x)])
+      (ref y))))
+ ("b"))
+
+(test-SL-result
+ ∅
+ (letrec ([(ref x) ("S" ("Z"))])
+   (match (ref x)
+     [("Z") ("a")]
+     [("S" _) ("b")]))
+ ("b"))
+
+(test-SL-result
+ ∅
+ (w-c-m ("a") ("1")
+        ((λ (x) x)
+         (w-c-m ("a") ("2")
+                (c-c-m [("a")]))))
+ ("cons"
+  ("cons" ("cons" ("a") ("1")) ("nil"))
+  ("cons" ("cons" ("cons" ("a") ("2")) ("nil"))
+          ("nil"))))
+
+(test-SL-result
+ ∅
+ (w-c-m ("a") ("1")
+        (w-c-m ("b") ("2")
+               (c-c-m [("a") ("b")])))
+ ("cons" ("cons" ("cons" ("b") ("2"))
+                 ("cons" ("cons" ("a") ("1")) ("nil")))
+         ("nil")))
+
+(test-SL-result
+ ∅
+ (w-c-m ("a") ("1")
+        (w-c-m ("b") ("2")
+               (c-c-m [("b") ("a")])))
+ ("cons" ("cons" ("cons" ("b") ("2"))
+                 ("cons" ("cons" ("a") ("1")) ("nil")))
+         ("nil")))
+
+(test-SL-result
+ ∅
+ (w-c-m ("a") ("1")
+        (c-c-m [("b") ("a")]))
+ ("cons" ("cons" ("cons" ("a") ("1")) ("nil"))
+         ("nil")))
+
+(test-SL-result
+ ∅
+ (w-c-m ("a") ("1") 
+        ((λ (x) x)
+         ((λ (x) x)
+          ((λ (x) x)
+           (w-c-m ("a") ("2")
+                  (w-c-m ("b") ("1")
+                         (c-c-m [("a") ("b")])))))))
+ ("cons"
+  ("cons" ("cons" ("a") ("1")) ("nil"))
+  ("cons" ("nil")
+          ("cons" ("nil")
+                  ("cons"
+                   ("cons"
+                    ("cons" ("b") ("1"))
+                    ("cons" ("cons" ("a") ("2"))
+                            ("nil")))
+                   ("nil"))))))
+
+(test-SL-result
+ ∅
+ (w-c-m ("a") ("1") 
+        ((λ (x) x)
+         (c-c-m [("a")])))
+ ("cons"
+  ("cons" ("cons" ("a") ("1")) ("nil"))
+  ("cons" ("nil") ("nil"))))
+
+(test-SL-result
+ ∅
+ ((λ (_)
+    ((λ (x) (x x))
+     (λ (x) (x x))))
+  (abort ("Z")))
+ ("Z"))
+
+(test-SL-result
+ ∅
+ ((λ (x)
+    (match x
+      [("Z") ("a")]
+      [("S" _) ("b")]))
+  (call/cc
+   (λ (k)
+     ((λ (_)
+        ((λ (x) (x x))
+         (λ (x) (x x))))
+      (k ("Z"))))))
+ ("a"))
+
+(test-SL-result
+ ∅
+ ((λ (x) ("S" ("S" x)))
+  (letrec ([(ref k) (κ ((λ (x) ("S" x)) hole))])
+    ((ref k) ("Z"))))
+ ("S" ("Z")))
+
+(test-SL-result
+ ∅
+ ((λ (x)
+    (match ("b" x)
+      [("b" x) x]))
+  ("a"))
+ ("a"))
+
+(test-->>
+ -->SL
+ #:cycles-ok
+ (term
+  (∅
+   /
+   ((λ (t) (t t))
+    (call/cc (λ (x) (call/cc x)))))))
+
+;; fact
+(define fact-impl
+   `(λ (n)
+      ,(:if `((ref =) n ,(num 0))
+            (:let 'marks '(c-c-m [("fact")])
+                  '(abort marks))
+            `(w-c-m ("fact") n
+                  ,(:let 'sub1-fact
+                         (:let 'sub1 `((ref -) n ,(num 1))
+                               `((ref fact) sub1))
+                         `((ref *) n sub1-fact))))))
+ (define fact-tr-impl
+   `(λ (n a)
+      ,(:if `((ref =) n ,(num 0))
+            (:let 'marks '(c-c-m [("fact")])
+                  '(abort marks))
+            `(w-c-m ("fact") n
+                    ,(:let 'sub1 `((ref -) n ,(num 1))
+                           (:let 'multa `((ref *) n a)
+                                 `((ref fact-tr) sub1 multa)))))))
+ (define (test-fact n)
+   (test-SL-result
+    ∅
+    ,(with-arith
+      `(letrec ([(ref fact) ,fact-impl])
+         ((ref fact) ,(num n))))
+    ,(lst (append (build-list n (λ (i) (term ("cons" ("cons" ("fact") ,(num (- n i))) ("nil")))))
+                  (list (term ("nil")) ; frame computing 1 * fact(0)
+                        (term ("nil"))))))) ; frame that names c-c-m result
+ (define (test-fact-tr n)
+   (test-SL-result
+    ∅
+    ,(with-arith
+      `(letrec ([(ref fact-tr) ,fact-tr-impl])
+         ((ref fact-tr) ,(num n) ,(num 1))))
+    ,(lst (list (term ("cons" ("cons" ("fact") ,(num 1)) ("nil")))
+                (term ("nil")))))) ; frame that names c-c-m result
+ (for ([i (in-range 1 4)]) (test-fact i))
+ (for ([i (in-range 1 4)]) (test-fact-tr i))
+
+;;; Values
+(test-->> -->SL
+          '(∅ / (λ (x) x))
+          '(∅ / (λ (x) x)))
+(test-->> -->SL
+          '(∅ / ("nil"))
+          '(∅ / ("nil")))
+(test-->> -->SL
+          '(∅ / ("S" ("0")))
+          '(∅ / ("S" ("0"))))
+(test-->> -->SL
+          '(∅ / (ref x))
+          '(∅ / (ref x)))
+
+;;; Applications
+(test-->> -->SL 
+          '(∅ / ((λ (x) x) ("nil")))
+          '(∅ / ("nil")))
+
+;;; Store applications
+(test-->> -->SL
+          '((∅ [(ref x) ↦ (λ (x) ("nil"))])
+            /
+            ((ref x) ("0")))
+          '((∅ [(ref x) ↦ (λ (x) ("nil"))])
+            /
+            ("nil")))
+
+;;; Letrec
+(test-->> -->SL
+          '(∅ / (letrec ([(ref x) (λ (x) ("nil"))])
+                  ("foo")))
+          '((∅ [(ref x) ↦ (λ (x) ("nil"))])
+            /
+            ("foo")))
+(test-->> -->SL
+          '(∅ / (letrec ([(ref x) (λ (x) ("nil"))])
+                  ((ref x) ("0"))))
+          '((∅ [(ref x) ↦ (λ (x) ("nil"))])
+            /
+            ("nil")))
+
+;;; match
+(test-->> -->SL
+          '(∅ / (match ("S" ("0"))
+                  [("S" n) n]
+                  [("0") ("0")]))
+          '(∅ / ("0")))
+(test-->> -->SL
+          '(∅ / (match ("S" ("0"))
+                  [("0") ("0")]
+                  [("S" n) n]))
+          '(∅ / ("0")))
+
+; Store match
+(test-->> -->SL
+          '(∅ / (letrec ([(ref x) ("S" ("0"))])
+                  (match (ref x)
+                    [("S" n) n]
+                    [("0") ("0")])))
+          '((∅ [(ref x) ↦ ("S" ("0"))])
+            /
+            ("0")))
+
+;; w-c-m
+(test-->> -->SL
+          `(∅ / (w-c-m ("k") ,(num 1) ,(num 2)))
+          `(∅ / ,(num 2)))
+(test-->> -->SL
+          `(∅ / (w-c-m ("k") ,(num 1) (w-c-m ("k") ,(num 3) ,(num 2))))
+          `(∅ / ,(num 2)))
+(test-->> -->SL
+          `(∅ / (w-c-m ("k") ,(num 1) ((λ (x) x) ,(num 2))))
+          `(∅ / ,(num 2)))
+
+;; c-c-m
+(test-->> -->SL
+          `(∅ / (c-c-m [("k")]))
+          `(∅ / ("cons" ("nil") ("nil"))))
+(test-->> -->SL
+          `(∅ / (w-c-m ("k") ,(num 1) (c-c-m [("k")])))
+          `(∅ / ("cons" ("cons" ("cons" ("k") ,(num 1)) ("nil")) ("nil"))))
+(test-->> -->SL
+          `(∅ / (w-c-m ("k") ,(num 1) (w-c-m ("k") ,(num 2) (c-c-m [("k")]))))
+          `(∅ / ("cons" ("cons" ("cons" ("k") ,(num 2)) ("nil")) ("nil"))))
+(test-->> -->SL
+          `(∅ / (w-c-m ("k") ,(num 1) ((λ (x) x) (w-c-m ("k") ,(num 2) (c-c-m [("k")])))))
+          `(∅ / ("cons" ("cons" ("cons" ("k") ,(num 1)) ("nil"))
+                        ("cons" ("cons" ("cons" ("k") ,(num 2)) ("nil"))
+                                ("nil")))))
+
+(test-->> -->SL
+          `(∅ / (w-c-m ("k1") ,(num 1) (c-c-m [("k1") ("k2")])))
+          `(∅ / ("cons" ("cons" ("cons" ("k1") ,(num 1)) ("nil")) ("nil"))))
+(test-->> -->SL
+          `(∅ / (w-c-m ("k1") ,(num 1) (w-c-m ("k2") ,(num 2) (c-c-m [("k1") ("k2")]))))
+          `(∅ / ("cons" ("cons" ("cons" ("k2") ,(num 2))
+                                ("cons" ("cons" ("k1") ,(num 1))
+                                        ("nil")))
+                        ("nil"))))
+
+;; abort
+(test-->> -->SL
+          `(∅ / (abort ,(num 2)))
+          `(∅ / ,(num 2)))
+(test-->> -->SL
+          `(∅ / ((λ (x) x) (abort ,(num 2))))
+          `(∅ / ,(num 2)))
+
+;; arith
+(test-->> -->SL
+          `(∅ / ,(:let 'x (num 1) 'x))
+          `(∅ / ,(num 1)))
+(test-SL-result ∅ ,(with-arith (num 1)) ,(num 1))
+(test-SL-result ∅ ,(with-arith `((ref +) ,(num 1) ,(num 1))) ,(num 2))
+(test-SL-result ∅ ,(with-arith `((ref *) ,(num 2) ,(num 2))) ,(num 4))
+(test-SL-result ∅ ,(with-arith `((ref =) ,(num 2) ,(num 2))) ("#t"))
+(test-SL-result ∅ ,(with-arith `((ref =) ,(num 2) ,(num 3))) ("#f"))
+(test-SL-result ∅ ,(with-arith `((ref -) ,(num 3) ,(num 2))) ,(num 1))
+(test-SL-result ∅ ,(with-arith (:if '("#t") (num 1) (num 2))) ,(num 1))
+(test-SL-result ∅ ,(with-arith (:if '("#f") (num 1) (num 2))) ,(num 2))
+
+;; call/cc
+(test-->> -->SL
+          `(∅ / (call/cc (λ (k) (k ("v")))))
+          `(∅ / ("v")))
+(test-->> -->SL
+          `(∅ / (call/cc (λ (k) 
+                           ((λ (x) ("x"))
+                            (k ("v"))))))
+          `(∅ / ("v")))
+
+;; call/cc + w-c-m
+(test-->> -->SL
+          `(∅ / (w-c-m ("k") ("v1")
+                       ((λ (f) (f ("unit")))
+                        (call/cc (λ (k)
+                                   (w-c-m ("k") ("v2")
+                                          (k (λ (x) (c-c-m [("k")])))))))))
+          `(∅ / ("cons" ("cons" ("cons" ("k") ("v1")) ("nil")) ("nil"))))
+
+(test-->> -->SL
+          `(∅ / (w-c-m ("k") ("v1")
+                     ((λ (f) (f ("unit")))
+                      (call/cc (λ (k)
+                                 (w-c-m ("k") ("v2")
+                                      ((λ (cms)
+                                         (k (λ (x) cms)))
+                                       (c-c-m [("k")]))))))))
+          `(∅ / ("cons" ("cons" ("cons" ("k") ("v1")) ("nil"))
+                        ("cons" ("cons" ("cons" ("k") ("v2")) ("nil"))
+                                ("cons" ("nil")
+                                        ("nil"))))))
\ No newline at end of file
diff --git a/collects/redex/examples/cont-mark-transform/SL-semantics.rkt b/collects/redex/examples/cont-mark-transform/SL-semantics.rkt
new file mode 100644
index 0000000000..10e458ad18
--- /dev/null
+++ b/collects/redex/examples/cont-mark-transform/SL-semantics.rkt
@@ -0,0 +1,126 @@
+#lang racket
+
+(require "SL-syntax.rkt"
+         redex)
+(provide -->SL χ)
+
+(define -->SL
+  (reduction-relation
+   SL #:domain (Σ / e)
+   (--> (Σ / (in-hole E ((λ (x ..._1) e) v ..._1)))
+        (Σ / (in-hole E (subst-n (x v) ... e)))
+        "1")
+   (--> (Σ / (in-hole E (match (K v ...) l ...)))
+        (Σ / (in-hole E (subst-n (x v) ... e)))
+        ; The match must be unique, according to Fig. 5
+        (where ([(K x ...) e]) (matches (K v ...) l ...))
+        "2")
+   (--> (Σ / (in-hole E (letrec ([σ v] ...) e)))
+        ((store-set Σ [σ ↦ v] ...) / (in-hole E e))
+        "3")
+   (--> (Σ / (in-hole E (σ v ...)))
+        (Σ / (in-hole E (subst-n (x v) ... e)))
+        (where (λ (x ...) e) (store-lookup Σ σ))
+        (side-condition (= (length (term (v ...))) (length (term (x ...)))))
+        "4")
+   (--> (Σ / (in-hole E_1 (σ v)))
+        (Σ / (in-hole E_2 v))
+        (where (κ E_2) (store-lookup Σ σ))
+        "4’")
+   (--> (Σ / (in-hole E (match σ l ...)))
+        (Σ / (in-hole E (match (store-lookup Σ σ) l ...)))
+        "5")
+   (--> (Σ / (in-hole E (w-c-m v_k v_1
+                               (in-hole C (w-c-m v_k v_2 e)))))
+        (Σ / (in-hole E (w-c-m v_k v_2 (in-hole C e))))
+        (side-condition (term (no-dup-keys C (v_k))))
+        "6")
+   (--> (Σ / (in-hole E (w-c-m v_k v_1 v_2)))
+        (Σ / (in-hole E v_2))
+        "7")
+   (--> (Σ / (in-hole E (c-c-m [v ...])))
+        (Σ / (in-hole E (χ (v ...) E ("nil"))))
+        "8")
+   (--> (Σ / (in-hole E (abort e)))
+        (Σ / e)
+        "9")
+   (--> (Σ / (in-hole E (call/cc v)))
+        (Σ / (in-hole E (v (κ E))))
+        "*")
+   (--> (Σ / (in-hole E_1 ((κ E_2) v)))
+        (Σ / (in-hole E_2 v))
+        "#")))
+
+(define-metafunction SL
+  [(matches (K v ...)) ()]
+  [(matches 
+    (K v ..._1)
+    [(K x ..._1) e]
+    l ...)
+   ([(K x ...) e] l_i ...)
+   (where (l_i ...) (matches (K v ...) l ...))]
+  [(matches 
+    (K v ..._1)
+    l_0 l_1 ...)
+   (l_i ...)
+   (where (l_i ...) (matches (K v ...) l_1 ...))])
+
+(define-metafunction SL
+  [(store-set Σ) Σ]
+  [(store-set Σ [σ_0 ↦ v_0] [σ_1 ↦ v_1] ...)
+   (store-set (Σ [σ_0 ↦ v_0]) [σ_1 ↦ v_1] ...)])
+
+(define-metafunction SL
+  [(store-lookup (Σ [σ ↦ v]) σ) v]
+  [(store-lookup (Σ [σ_1 ↦ v]) σ_2)
+   (store-lookup Σ σ_2)])
+
+(define-metafunction SL
+  [(χ (v_0 ...) E)
+   (χ (v_0 ...) E ("nil"))]
+  [(χ (v_0 ...) hole v_l) ("cons" v_l ("nil"))]
+  [(χ (v_0 ...) (v_i ... E) v_l)
+   ("cons" v_l (χ (v_0 ...) E ("nil")))]
+  [(χ (v_0 ... v_k v_k+1 ...) (w-c-m v_k v_v E) v_l)
+   (χ (v_0 ... v_k v_k+1 ...) E ("cons" ("cons" v_k v_v) v_l))]
+  [(χ (v_0 ...) (w-c-m v_k v_v E) v_l)
+   (χ (v_0 ...) E v_l)])
+
+(define-metafunction SL
+  [(subst-n (x_1 any_1) (x_2 any_2) ... any_3)
+   (subst x_1 any_1 (subst-n (x_2 any_2) ... any_3))]
+  [(subst-n any_3) any_3])
+
+(define-metafunction SL
+  ;; x_1 bound, so don't continue in body 
+  [(subst x_1 any_1 (λ (x_2 ... x_1 x_3 ...) any_2))
+   (λ (x_2 ... x_1 x_3 ...) any_2)]
+  ;; general purpose capture avoiding case 
+  [(subst x_1 any_1 (λ (x_2 ...) any_2))
+   (λ (x_new ...) (subst x_1 any_1 (subst-vars (x_2 x_new) ... any_2)))
+   (where (x_new ...) ,(variables-not-in (term (x_1 any_1 any_2)) (term (x_2 ...))))]
+  ;; replace x_1 with e_1 
+  [(subst x_1 any_1 x_1) any_1]
+  ;; x_1 and x_2 are different, so don't replace 
+  [(subst x_1 any_1 x_2) x_2]
+  ;; match
+  [(subst x_1 any_1 (match a [(K_0 x_0 ...) e_0] ...))
+   (match (subst x_1 any_1 a)
+     [(K_0 x_0’ ...) e_0’] 
+     ...)
+   (where 
+    ((λ (x_0’ ...) e_0’) ...)
+    ((subst x_1 any_1 (λ (x_0 ...) e_0)) ...))]
+  ;; ref
+  [(subst x any σ) σ]
+  ;; the last cases cover all other expressions 
+  [(subst x_1 any_1 (any_2 ...)) ((subst x_1 any_1 any_2) ...)]
+  [(subst x_1 any_1 any_2) any_2])
+
+(define-metafunction SL
+  [(subst-vars (x_1 any_1) x_1) any_1]
+  [(subst-vars (x_1 any_1) (any_2 ...)) ((subst-vars (x_1 any_1) any_2) ...)]
+  [(subst-vars (x_1 any_1) any_2) any_2]
+  [(subst-vars (x_1 any_1) (x_2 any_2) ... any_3)
+   (subst-vars (x_1 any_1) (subst-vars (x_2 any_2) ... any_3))]
+  [(subst-vars any) any])
\ No newline at end of file
diff --git a/collects/redex/examples/cont-mark-transform/SL-syntax.rkt b/collects/redex/examples/cont-mark-transform/SL-syntax.rkt
new file mode 100644
index 0000000000..8c1fad5977
--- /dev/null
+++ b/collects/redex/examples/cont-mark-transform/SL-syntax.rkt
@@ -0,0 +1,44 @@
+#lang racket
+
+(require "TL-syntax.rkt"
+         redex)
+(provide SL no-dup-keys)
+
+(define-extended-language SL TL
+  (e ....
+     (call/cc w))
+  (v ....
+     (κ (hide-hole E)))
+  
+  (D (w-c-m v v D)
+     hole
+     (v ... D))
+  (E (side-condition D_1 (term (no-dup-keys D_1 ()))))
+  
+  ; used in the marks collapsing rule (6)
+  (C (w-c-m v v C)
+     hole)
+  
+  ; used in translation
+  (r (a ...)
+     (letrec ([σ w] ...) e)
+     (w-c-m a a a)
+     (c-c-m [a ...])
+     (match a l ...)
+     (abort e)
+     (call/cc e))
+  (T (w-c-m a a T)
+     hole
+     (a ... T))
+  (k v
+     #f))
+
+(define-metafunction SL
+  [(no-dup-keys hole (v ...)) 
+   #t]
+  [(no-dup-keys (w-c-m v_i v D) (v_0 ... v_i v_i+1 ...))
+   #f]
+  [(no-dup-keys (w-c-m v_i v D) (v_0 ...))
+   (no-dup-keys D (v_i v_0 ...))]
+  [(no-dup-keys (v ... D) (v_0 ...))
+   (no-dup-keys D ())])
diff --git a/collects/redex/examples/cont-mark-transform/TL-semantics-test.rkt b/collects/redex/examples/cont-mark-transform/TL-semantics-test.rkt
new file mode 100644
index 0000000000..dc1730d102
--- /dev/null
+++ b/collects/redex/examples/cont-mark-transform/TL-semantics-test.rkt
@@ -0,0 +1,21 @@
+#lang racket
+
+(require "TL-semantics.rkt"
+         "common.rkt"
+         redex)
+
+(test-TL-result
+ ∅
+ ((λ (x) x) (λ (x) x))
+ (λ (x) x))
+
+(test-TL-stuck
+ ∅
+ (call/cc (λ (x) x)))
+
+(test-predicate
+ (curry regexp-match? #rx"not defined")
+ (with-handlers ([exn:fail? exn-message])
+   (apply-reduction-relation
+    -->TL
+    (term (∅ / ((κ hole) (λ (x) x)))))))
diff --git a/collects/redex/examples/cont-mark-transform/TL-semantics.rkt b/collects/redex/examples/cont-mark-transform/TL-semantics.rkt
new file mode 100644
index 0000000000..4bf7074a51
--- /dev/null
+++ b/collects/redex/examples/cont-mark-transform/TL-semantics.rkt
@@ -0,0 +1,19 @@
+#lang racket
+
+(require "TL-syntax.rkt"
+         "SL-syntax.rkt"
+         "SL-semantics.rkt"
+         redex)
+
+(provide -->TL)
+
+(define -->TL
+  (extend-reduction-relation
+   -->SL SL #:domain (Σ / (side-condition e_1 (TL-expr? (term e_1))))
+   (--> any any
+        (side-condition #f)
+        "*")
+   (--> any any
+        (side-condition #f)
+        "#")))
+(define TL-expr? (redex-match TL e))
\ No newline at end of file
diff --git a/collects/redex/examples/cont-mark-transform/TL-syntax.rkt b/collects/redex/examples/cont-mark-transform/TL-syntax.rkt
new file mode 100644
index 0000000000..df8ac09a17
--- /dev/null
+++ b/collects/redex/examples/cont-mark-transform/TL-syntax.rkt
@@ -0,0 +1,30 @@
+#lang racket
+
+(require redex)
+(provide TL)
+
+(define-language TL
+  (e a
+     (a ... e)
+     (letrec ([σ v] ...) e)
+     (w-c-m a a e)
+     (c-c-m [a ...])
+     (match a l ...)
+     (abort e))
+  
+  (l [(K x ...) e])
+  (a w 
+     (K a ...))
+  (w v
+     x)
+  (v (λ (x ...) e)
+     (K v ...)
+     σ)
+  
+  (x variable-not-otherwise-mentioned)
+  (σ (ref variable))
+  
+  (Σ ∅
+     (Σ [σ ↦ v]))
+  
+  (K string))
\ No newline at end of file
diff --git a/collects/redex/examples/cont-mark-transform/all-test.rkt b/collects/redex/examples/cont-mark-transform/all-test.rkt
new file mode 100644
index 0000000000..56c8966aff
--- /dev/null
+++ b/collects/redex/examples/cont-mark-transform/all-test.rkt
@@ -0,0 +1,5 @@
+#lang racket
+
+(require "TL-semantics-test.rkt"
+         "SL-semantics-test.rkt"
+         "CMT-test.rkt")
diff --git a/collects/redex/examples/cont-mark-transform/common.rkt b/collects/redex/examples/cont-mark-transform/common.rkt
new file mode 100644
index 0000000000..05a698a5e6
--- /dev/null
+++ b/collects/redex/examples/cont-mark-transform/common.rkt
@@ -0,0 +1,78 @@
+#lang racket
+
+(require "SL-syntax.rkt" "SL-semantics.rkt"
+         "TL-syntax.rkt" "TL-semantics.rkt"
+         redex)
+
+(define ((make-eval --> value?) program)
+  (match (unique-normal-form program -->)
+    [(and state `(,_ / ,expr))
+     (if (value? expr)
+         (term (answer ,expr))
+         (raise (eval-undefined "stuck" (current-continuation-marks) program state)))]))
+(define-struct (eval-undefined exn:fail) (input stuck-state))
+(provide make-eval
+         (struct-out eval-undefined))
+
+(define-metafunction SL
+  [(answer (λ (x ...) e))
+   procedure]
+  [(answer (K v ...))
+   (K (answer v) ...)]
+  [(answer σ)
+   reference]
+  [(answer (κ E))
+   procedure])
+
+(define (unique-normal-form t R)
+  (match (let ([nfs '()]
+               [seen (set)])
+           (let recur ([u t] [s (max-normalization-steps)])
+             (when (negative? s)
+               (raise (normalization-timeout "too many steps" (current-continuation-marks))))
+             (unless (set-member? seen u)
+               (set! seen (set-add seen u))
+               (match (apply-reduction-relation R u)
+                 [(list) (set! nfs (cons u nfs))]
+                 [vs (for ([v vs]) (recur v (sub1 s)))])))
+           nfs)
+    [(list u) u]
+    [(list) (raise (normalization-timeout "no normal forms" (current-continuation-marks)))]
+    [_ (error 'unique-normal-form "distinct normal forms")]))
+(define max-normalization-steps (make-parameter +inf.0))
+(define-struct (normalization-timeout exn:fail) ())
+(provide max-normalization-steps
+         (struct-out normalization-timeout))
+
+(define-syntax (test-result stx)
+  (syntax-case stx ()
+    [(_ R Σ e v)
+     #`(match (unique-normal-form (term (Σ / e)) R)
+         [`(,_ / ,u)
+          #,(syntax/loc stx (test-equal u (term v)))])]))
+
+(define-syntax (test-stuck stx)
+  (syntax-case stx ()
+    [(_ R v? Σ e)
+     #`(match (unique-normal-form (term (Σ / e)) R)
+         [`(,_ / ,r)
+          #,(syntax/loc stx (test-predicate (negate v?) r))])]))
+
+(define-syntax-rule (define-test-forms language relation test-result-id test-stuck-id)
+  (begin
+    (define value? (redex-match language v))
+    (define-syntax-rule (test-result-id . args)
+      (test-result relation . args))
+    (define-syntax-rule (test-stuck-id . args)
+      (test-stuck relation value? . args))
+    (provide test-result-id test-stuck-id)))
+
+(define-test-forms SL -->SL test-SL-result test-SL-stuck)
+(define-test-forms TL -->TL test-TL-result test-TL-stuck)
+
+(define-metafunction SL
+  [(make-store) ∅]
+  [(make-store [any_1 any_2] any_3 ...)
+   ((make-store any_3 ...)
+    [(ref any_1) ↦ any_2])])
+(provide make-store)
\ No newline at end of file
diff --git a/collects/redex/examples/cont-mark-transform/randomized-tests.rkt b/collects/redex/examples/cont-mark-transform/randomized-tests.rkt
new file mode 100644
index 0000000000..8f14ce49f7
--- /dev/null
+++ b/collects/redex/examples/cont-mark-transform/randomized-tests.rkt
@@ -0,0 +1,232 @@
+#lang racket
+
+(require "SL-syntax.rkt" "SL-semantics.rkt"
+         "TL-syntax.rkt" "TL-semantics.rkt"
+         "CMT.rkt"
+         "common.rkt"
+         redex)
+(provide main same-result?)
+
+(define (main . args)
+  (define seed (add1 (random (sub1 (expt 2 31)))))
+  (define unique-decomp-tests #f)
+  (define CMT-range-all-tests #f)
+  (define CMT-range-rules-tests #f)
+  (define same-result-all-tests #f)
+  (define same-result-rules-tests #f)
+  
+  (command-line
+   #:argv args
+   #:once-each
+   ["--seed"
+    n
+    "Seed PRG with n"
+    (set! seed (string->number n))]
+   ["--unique-decomposition"
+    n
+    "Test unique decomposition of n expressions"
+    (set! unique-decomp-tests (string->number n))]
+   ["--CMT-range"
+    n
+    ("Test that CMT produces a TL expression for n expressions,"
+     "chosen from SL's e non-terminal")
+    (set! CMT-range-all-tests (string->number n))]
+   ["--CMT-range-rules"
+    n
+    ("Test that CMT produces a TL expression for n expressions,"
+     "chosen from the left-hand sides of -->SL")
+    (set! CMT-range-rules-tests (string->number n))]
+   ["--same-result"
+    n
+    ("Test that translation preserves meaning for n expression,"
+     "chosen from SL's e non-terminal")
+    (set! same-result-all-tests (string->number n))]
+   ["--same-result-rules"
+    n
+    ("Test that translation preserves meaning for n expression,"
+     "chosen from SL's e non-terminal")
+    (set! same-result-rules-tests (string->number n))])
+  
+  (printf "Random seed: ~s\n" seed)
+  
+  (when unique-decomp-tests
+    (test-unique-decomposition unique-decomp-tests))
+  (when CMT-range-all-tests
+    (test-CMT-range CMT-range-all-tests))
+  (when CMT-range-rules-tests
+    (test-CMT-range/rules CMT-range-rules-tests))
+  (when same-result-all-tests
+    (test-same-result same-result-all-tests))
+  (when same-result-rules-tests
+    (test-same-result/rules same-result-rules-tests)))
+
+;; Unique decomposition
+(define (test-unique-decomposition attempts)
+  (redex-check SL e (uniquely-decomposes? (term e)) #:attempts attempts))
+
+(define uniquely-decomposes?
+  (let ([a? (redex-match SL a)]
+        [decompositions (redex-match SL (in-hole T r))])
+    (λ (e)
+      (or (a? e)
+          (match (decompositions e)
+            [(list _) #t]
+            [_ #f])))))
+
+;; CMT produces TL expressions
+(define (test-CMT-range attempts)
+  (test-translation CMT-produces-TL?
+                    #:attempts attempts))
+
+(define (test-CMT-range/rules attempts)
+  (test-translation CMT-produces-TL? 
+                    #:attempts attempts 
+                    #:source -->SL/no-side-conds))
+
+(define CMT-produces-TL?
+  (let ([TL-e? (redex-match TL e)])
+    (λ (e) 
+      (TL-e? (term (CMT ,e))))))
+
+;; Translated programs have the same result
+(define (test-same-result attempts)
+  (test-translation same-result? 
+                    #:attempts attempts))
+
+(define (test-same-result/rules attempts)
+  (test-translation same-result?
+                    #:attempts attempts
+                    #:source -->SL/no-side-conds))
+
+(define (same-result? expr)
+  (let/ec return
+    (define SL-result
+      (with-handlers ([normalization-timeout? return]
+                      [eval-undefined? return])
+        (parameterize ([max-normalization-steps 1000])
+          (SL-eval (term (∅ / ,expr))))))
+    (define TL-result
+      (TL-eval (term (∅ / (translate ,expr)))))
+    (or (equal? SL-result TL-result)
+        (compares-incomparable-keys? expr))))
+
+(define SL-eval
+  (make-eval -->SL (redex-match SL v)))
+(define TL-eval
+  (make-eval -->TL (redex-match TL v)))
+
+;; Utilities
+(define-syntax-rule (test-translation predicate . kw-args)
+  (redex-check SL-gen (Σ / e) 
+               (predicate (term e))
+               #:prepare close-program . kw-args))
+
+(define-extended-language SL-gen SL
+  (σ (ref (variable-except resume restore-marks c-w-i-c-m map-set kont/ms equal? last)))
+  (K (side-condition string_1 (not (member (term string_1) '("square" "diamond")))))
+  
+  (K-tree (K K-tree ...)))
+
+(define -->SL/no-side-conds
+  ; Disables side-conditions on some rules.
+  (extend-reduction-relation
+   -->SL SL
+   (--> (Σ / (in-hole E (match (K v ...) l ...))) any "2")
+   (--> (Σ / (in-hole E (σ v ...))) any "4")
+   (--> (Σ / (in-hole E_1 (σ v))) any "4’")))
+
+(define close-program
+  (match-lambda
+    [`(,Σ / ,e)
+     `(,Σ / ,(close-expr e))]))
+
+(define close-expr
+  (let ([var? (redex-match SL x)]
+        [val? (redex-match SL v)])
+    (λ (expr)
+      ; 1. Considers refs to be bound only within the binding letrec.
+      ; 2. Avoids adding duplicate mark to an existing frame, since 
+      ; doing so (a) can make a continuation value syntactically invalid
+      ; and (b) can change the reduction rule that applies
+      (let recur ([expr expr] [vars (set)] [refs (set)] [keys (set)])
+        (match expr
+          [(? var?)
+           (if (set-empty? vars)
+               (if (set-empty? refs)
+                   (random-constant)
+                   `(ref ,(random-element refs)))
+               (if (set-member? vars expr)
+                   expr
+                   (random-element vars)))]
+          [`(ref ,σ)
+           (if (set-empty? refs)
+               (random-constant)
+               (if (set-member? refs σ)
+                   expr
+                   `(ref ,(random-element refs))))]
+          [`(w-c-m ,k ,v ,e)
+           (define k’
+             (if (val? k)
+                 k
+                 (let retry ([candidate (recur k vars refs keys)]
+                             [retries 0])
+                   (when (> retries 3)
+                     (error 'close "too many"))
+                   (if (set-member? keys candidate)
+                       (retry (list (first (random-constant)) candidate)
+                              (add1 retries))
+                       candidate))))
+           (define ext-keys
+             (if (val? k’)
+                 (set-add keys k’)
+                 keys))
+           `(w-c-m ,k’ ,(recur v vars refs (set))
+                   ,(recur e vars refs ext-keys))]
+          [`(letrec ([(ref ,σs) ,es] ...) ,e)
+           (define ext-refs (extend refs σs))
+           `(letrec ,(for/list ([e es] [σ σs])
+                               `[(ref ,σ) ,(recur e vars ext-refs (set))])
+              ,(recur e vars ext-refs (set)))]
+          [`(match ,e [(,ks ,xss ...) ,es] ...)
+           (define ext-vars (extend vars (apply append xss)))
+           `(match ,(recur e vars refs (set))
+              ,@(for/list ([xs xss] [e es] [k ks])
+                  `[(,k ,@xs) ,(recur e ext-vars refs (set))]))]
+          [`(λ ,xs ,e)
+           (define ext-vars (extend vars xs))
+           `(λ ,xs ,(recur e ext-vars refs (set)))]
+          [(? list?)
+           (map (λ (e) (recur e vars refs (set))) expr)]
+          [_ expr])))))
+
+(define (extend s xs)
+  (for/fold ([s s]) ([x xs])
+            (set-add s x)))
+
+(define random-constant
+  (let ([generate-K-tree (generate-term SL-gen K-tree)])
+    (λ () (generate-K-tree (random 3)))))
+
+(define (random-element xs)
+  (list-ref (set-map xs values) (random (set-count xs))))
+
+(define (compares-incomparable-keys? expr)
+  (define procedure? (redex-match SL (λ (x ...) e)))
+  (define continuation? (redex-match SL (κ E)))
+  (let/ec return
+    (apply-reduction-relation*
+     (extend-reduction-relation 
+      -->SL SL
+      (--> (Σ / (in-hole E (c-c-m [v ...])))
+           ,(if (andmap comparable? (term (v ...)))
+                (term (Σ / (in-hole E (χ (v ...) E ("nil")))))
+                (return #t))
+           "8"))
+     `(∅ / ,expr))
+    #f))
+
+(define comparable?
+  (let ()
+    (define-extended-language SL’ SL
+      (c σ (K c ...)))
+    (redex-match SL’ c)))
\ No newline at end of file
diff --git a/collects/redex/examples/cont-mark-transform/test-util.rkt b/collects/redex/examples/cont-mark-transform/test-util.rkt
new file mode 100644
index 0000000000..51451c2c51
--- /dev/null
+++ b/collects/redex/examples/cont-mark-transform/test-util.rkt
@@ -0,0 +1,84 @@
+#lang racket
+
+(require "common.rkt" redex)
+(provide (all-defined-out))
+
+(define (num n)
+  (if (zero? n)
+      `("0")
+      `("S" ,(num (sub1 n)))))
+
+(define (lst l)
+  (if (empty? l)
+      `("nil")
+      `("cons" ,(first l) ,(lst (rest l)))))
+
+(define (:let name named-expr body)
+  `((λ (,name) ,body)
+    ,named-expr))
+
+(define =-impl
+  `(λ (x y)
+     (match x
+       [("0") 
+        (match y
+          [("0") ("#t")]
+          [("S" yn) ("#f")])]
+       [("S" xn)
+        (match y
+          [("0") ("#f")]
+          [("S" yn) ((ref =) xn yn)])])))
+
+(define +-impl
+  `(λ (x y)
+     (match x
+       [("0") y]
+       [("S" xn)
+        ,(:let 'in '((ref +) xn y)
+               '("S" in))])))
+
+(define --impl
+  `(λ (n m)
+     (match n
+       [("0") n]
+       [("S" k) 
+        (match m
+          [("0") n]
+          [("S" l) ((ref -) k l)])])))
+
+(define *-impl
+  `(λ (n m)
+     (match n
+       [("0") ("0")]
+       [("S" p) ,(:let 'tmp '((ref *) p m)
+                       '((ref +) m tmp))])))
+
+(define if-impl
+  `(λ (cond true false)
+     (match cond
+       [("#t") (true)]
+       [("#f") (false)])))
+
+(define (with-arith e)
+  `(letrec
+       ([(ref =) ,=-impl]
+        [(ref +) ,+-impl]
+        [(ref -) ,--impl]
+        [(ref *) ,*-impl]
+        [(ref if) ,if-impl])
+     ,e))
+
+(define arith-store
+  (term
+   (make-store [= ,=-impl] 
+               [+ ,+-impl]
+               [- ,--impl]
+               [* ,*-impl]
+               [if ,if-impl])))
+
+(define (:if cond true false)
+  (:let 'cond-val cond
+        `((ref if)
+          cond-val
+          (λ () ,true)
+          (λ () ,false))))
\ No newline at end of file
diff --git a/collects/redex/tests/run-tests.rkt b/collects/redex/tests/run-tests.rkt
index 6fe9b9bb44..84c63eb964 100644
--- a/collects/redex/tests/run-tests.rkt
+++ b/collects/redex/tests/run-tests.rkt
@@ -32,6 +32,7 @@
          "../examples/racket-machine/reduction-test.ss"
          "../examples/racket-machine/verification-test.ss"
          "../examples/delim-cont/test.rkt"
+         "../examples/cont-mark-transform/all-test.rkt"
          ("../examples/r6rs/r6rs-tests.ss" main))
        '())))