diff --git a/benchmarks/README.md b/benchmarks/README.md
new file mode 100644
index 000000000..2feb099e6
--- /dev/null
+++ b/benchmarks/README.md
@@ -0,0 +1,7 @@
+# To run Coalton Benchmarks:
+
+`(ql:quickload :coalton/benchmarks)` or `(asdf:load-system :coalton/benchmarks)`
+
+`(in-package #:coalton-benchmarks)`
+
+`(run-benchmarks)`
\ No newline at end of file
diff --git a/benchmarks/gabriel-benchmarks/stak.lisp b/benchmarks/gabriel-benchmarks/stak.lisp
new file mode 100644
index 000000000..87c793580
--- /dev/null
+++ b/benchmarks/gabriel-benchmarks/stak.lisp
@@ -0,0 +1,78 @@
+;;;; gabriel-benchmarks/stak.lisp
+;;;;
+;;;;
+
+(in-package #:coalton-benchmarks)
+
+(define-benchmark stak ()
+  (declare (optimize speed))
+  (loop :repeat 1000
+        :do (with-benchmark-sampling
+              (coalton-benchmarks/native:stak 18 12 6)))
+  (report trivial-benchmark::*current-timer*))
+
+(define-benchmark stak-lisp ()
+  (declare (optimize speed))
+  (loop :repeat 1000
+        :do (with-benchmark-sampling
+              (lisp-stak 18 12 6)))
+  (report trivial-benchmark::*current-timer*))
+
+;;;
+;;;
+;;;
+
+
+(defvar x)
+(defvar y)
+(defvar z)
+
+(declaim (ftype (function () fixnum) stak-aux))
+(defun stak-aux ()
+  (if (not (< y x))
+      z
+      (let ((x (let ((x (1- x))
+                     (y y)
+                     (z z))
+                 (stak-aux)))
+            (y (let ((x (1- y))
+                     (y z)
+                     (z x))
+                 (stak-aux)))
+            (z (let ((x (1- z))
+                     (y x)(z y))
+                 (stak-aux))))
+        (stak-aux))))
+
+(declaim (ftype (function (fixnum) fixnum) lisp-stak))
+(defun lisp-stak (x y z)
+  (stak-aux))
+
+;;;
+;;;
+;;;
+
+
+(cl:in-package #:coalton-benchmarks/native)
+
+(cl:declaim (cl:optimize (cl:speed 3) (cl:safety 0)))
+
+(coalton-toplevel
+
+ (declare stak (IFix -> IFix -> IFix -> IFix))
+ (define (stak x y z)
+     (if (not (< y x))
+         z
+         (let ((x1 (let ((x2 (1- x))
+                         (y2 y)
+                         (z2 z))
+                     (stak x2 y2 z2)))
+               (y1 (let ((x2 (1- y))
+                         (y2 z)
+                         (z2 x))
+                     (stak x2 y2 z2)))
+               (z1 (let ((x2 (1- z))
+                         (y2 x)
+                         (z2 y))
+                     (stak x2 y2 z2))))
+           (stak x1 y1 z1)))))
diff --git a/benchmarks/gabriel-benchmarks/tak.lisp b/benchmarks/gabriel-benchmarks/tak.lisp
new file mode 100644
index 000000000..d5322c11c
--- /dev/null
+++ b/benchmarks/gabriel-benchmarks/tak.lisp
@@ -0,0 +1,41 @@
+;;;; gabriel-benchmarks/tak.lisp
+;;;;
+;;;; 
+
+(cl:in-package #:coalton-benchmarks)
+
+(define-benchmark tak ()
+  (declare (optimize speed))
+  (loop :repeat 1000
+        :do (with-benchmark-sampling
+              (coalton:coalton (coalton-benchmarks/native:tak 18 12 6))))
+  (report trivial-benchmark::*current-timer*))
+
+(define-benchmark tak-lisp ()
+  (declare (optimize speed))
+  (loop :repeat 1000
+        :do (with-benchmark-sampling
+              (lisp-tak 18 12 6)))
+  (report trivial-benchmark::*current-timer*))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) lisp-tak))
+(defun lisp-tak (x y z)
+  (if (not (< y x))
+      z
+      (lisp-tak (lisp-tak (1- x) y z)
+                (lisp-tak (1- y) z x)
+                (lisp-tak (1- z) x y))))
+
+(cl:in-package #:coalton-benchmarks/native)
+
+(cl:declaim (cl:optimize (cl:speed 3) (cl:safety 0)))
+
+(coalton-toplevel
+
+  (declare tak (IFix -> IFix -> IFix -> IFix))
+  (define (tak x y z)
+    (if (not (< y x))
+        z
+        (tak (tak (1- x) y z)
+             (tak (1- y) z x)
+             (tak (1- z) x y)))))
diff --git a/benchmarks/gabriel-benchmarks/takl.lisp b/benchmarks/gabriel-benchmarks/takl.lisp
new file mode 100644
index 000000000..23e3fdd87
--- /dev/null
+++ b/benchmarks/gabriel-benchmarks/takl.lisp
@@ -0,0 +1,88 @@
+;;;; gabriel-benchmarks/takl.lisp
+;;;;
+;;;;
+
+(cl:in-package #:coalton-benchmarks)
+
+(define-benchmark takl ()
+  (declare (optimize speed))
+  (loop :repeat 1000
+        :do (with-benchmark-sampling
+              (coalton-benchmarks/native:takl 18 12 6)))
+  (report trivial-benchmark::*current-timer*))
+
+(define-benchmark takl-lisp ()
+  (declare (optimize speed))
+  (loop :repeat 1000
+        :do (with-benchmark-sampling
+              (lisp-takl 18 12 6)))
+  (report trivial-benchmark::*current-timer*))
+
+;;;
+;;;
+;;;
+
+(declaim (ftype (function (fixnum) list) listn))
+(defun listn (n)
+  (if (not (= 0 n))
+      (cons n (listn (1- n)))))
+
+(declaim (ftype (function (list list) boolean)))
+(defun shorterp (x y)
+  (and y (or (null x)
+             (shorterp (cdr x)
+                       (cdr y)))))
+
+(declaim (ftype (function (list list list) list)))
+(defun mas (x y z)
+  (if (not (shorterp y x))
+      z
+      (mas (mas (cdr x)
+                y z)
+           (mas (cdr y)
+                z x)
+           (mas (cdr z)
+                x y))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) list)))
+(defun lisp-takl (x y z)
+  (mas (listn x) (listn y) (listn z)))
+
+;;;
+;;;
+;;;
+
+
+(cl:in-package #:coalton-benchmarks/native)
+
+(cl:declaim (cl:optimize (cl:speed 3) (cl:safety 0)))
+
+(coalton-toplevel
+
+  (declare listn (UFix -> (List UFix)))
+  (define (listn n)
+    (if (not (== n 0))
+        (Cons n (listn (1- n)))
+        Nil))
+
+  (declare shorterp ((List UFix) -> (List UFix) -> Boolean))
+  (define (shorterp x y)
+    (and (not (list:null? y))
+         (or (list:null? x)
+             (shorterp (list:cdr x)
+                       (list:cdr y)))))
+
+  (declare mas ((List UFix) -> (List UFix) -> (List UFix) -> (List UFix)))
+  (define (mas x y z)
+    (if (not (shorterp y x))
+        z
+        (mas (mas (list:cdr x)
+                  y z)
+             (mas (list:cdr y)
+                  z x)
+             (mas (list:cdr z)
+                  x y))))
+
+  (declare takl (UFix -> UFix -> UFix -> (List UFix)))
+  (define (takl x y z)
+    (mas (listn x) (listn y) (listn z))))
diff --git a/benchmarks/gabriel-benchmarks/takr.lisp b/benchmarks/gabriel-benchmarks/takr.lisp
new file mode 100644
index 000000000..a8ce2bb5a
--- /dev/null
+++ b/benchmarks/gabriel-benchmarks/takr.lisp
@@ -0,0 +1,1434 @@
+;;;; gabriel-benchmarks/takl.lisp
+;;;;
+;;;;
+
+(cl:in-package #:coalton-benchmarks)
+
+(define-benchmark takr ()
+  (declare (optimize speed))
+  (loop :repeat 1000
+        :do (with-benchmark-sampling
+              (coalton-benchmarks/native:takr 18 12 6)))
+  (report trivial-benchmark::*current-timer*))
+
+(define-benchmark takr-lisp ()
+  (declare (optimize speed))
+  (loop :repeat 1000
+        :do (with-benchmark-sampling
+              (lisp-takr 18 12 6)))
+  (report trivial-benchmark::*current-timer*))
+
+;;;
+;;;
+;;;
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) lisp-takr))
+(defun lisp-takr (x y z)
+  (cond ((>= y x) z)
+        (t (tak1 (tak37 (- x 1) y z)
+                 (tak11 (- y 1) z x)
+                 (tak17 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak1))
+(defun tak1 (x y z)
+   (cond ((>= y x) z)
+         (t (tak2 (tak74 (- x 1) y z)
+                  (tak22 (- y 1) z x)
+                  (tak34 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak2))
+(defun tak2 (x y z)
+   (cond ((>= y x) z)
+         (t (tak3 (tak11 (- x 1) y z)
+                  (tak33 (- y 1) z x)
+                  (tak51 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak3))
+(defun tak3 (x y z)
+   (cond ((>= y x) z)
+         (t (tak4 (tak48 (- x 1) y z)
+                  (tak44 (- y 1) z x)
+                  (tak68 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak4))
+(defun tak4 (x y z)
+   (cond ((>= y x) z)
+         (t (tak5 (tak85 (- x 1) y z)
+                  (tak55 (- y 1) z x)
+                  (tak85 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak5))
+(defun tak5 (x y z)
+   (cond ((>= y x) z)
+         (t (tak6 (tak22 (- x 1) y z)
+                  (tak66 (- y 1) z x)
+                  (tak2 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak6))
+(defun tak6 (x y z)
+   (cond ((>= y x) z)
+         (t (tak7 (tak59 (- x 1) y z)
+                  (tak77 (- y 1) z x)
+                  (tak19 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak7))
+(defun tak7 (x y z)
+   (cond ((>= y x) z)
+         (t (tak8 (tak96 (- x 1) y z)
+                  (tak88 (- y 1) z x)
+                  (tak36 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak8))
+(defun tak8 (x y z)
+   (cond ((>= y x) z)
+         (t (tak9 (tak33 (- x 1) y z)
+                  (tak99 (- y 1) z x)
+                  (tak53 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak9))
+(defun tak9 (x y z)
+   (cond ((>= y x) z)
+         (t (tak10 (tak70 (- x 1) y z)
+                   (tak10 (- y 1) z x)
+                   (tak70 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak10))
+(defun tak10 (x y z)
+   (cond ((>= y x) z)
+         (t (tak11 (tak7 (- x 1) y z)
+                   (tak21 (- y 1) z x)
+                   (tak87 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak11))
+(defun tak11 (x y z)
+   (cond ((>= y x) z)
+         (t (tak12 (tak44 (- x 1) y z)
+                   (tak32 (- y 1) z x)
+                   (tak4 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak12))
+(defun tak12 (x y z)
+   (cond ((>= y x) z)
+         (t (tak13 (tak81 (- x 1) y z)
+                   (tak43 (- y 1) z x)
+                   (tak21 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak13))
+(defun tak13 (x y z)
+   (cond ((>= y x) z)
+         (t (tak14 (tak18 (- x 1) y z)
+                   (tak54 (- y 1) z x)
+                   (tak38 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak14))
+(defun tak14 (x y z)
+   (cond ((>= y x) z)
+         (t (tak15 (tak55 (- x 1) y z)
+                   (tak65 (- y 1) z x)
+                   (tak55 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak15))
+(defun tak15 (x y z)
+   (cond ((>= y x) z)
+         (t (tak16 (tak92 (- x 1) y z)
+                   (tak76 (- y 1) z x)
+                   (tak72 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak16))
+(defun tak16 (x y z)
+   (cond ((>= y x) z)
+         (t (tak17 (tak29 (- x 1) y z)
+                   (tak87 (- y 1) z x)
+                   (tak89 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak17))
+(defun tak17 (x y z)
+   (cond ((>= y x) z)
+         (t (tak18 (tak66 (- x 1) y z)
+                   (tak98 (- y 1) z x)
+                   (tak6 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak18))
+(defun tak18 (x y z)
+   (cond ((>= y x) z)
+         (t (tak19 (tak3 (- x 1) y z)
+                   (tak9 (- y 1) z x)
+                   (tak23 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak19))
+(defun tak19 (x y z)
+   (cond ((>= y x) z)
+         (t (tak20 (tak40 (- x 1) y z)
+                   (tak20 (- y 1) z x)
+                   (tak40 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak20))
+(defun tak20 (x y z)
+   (cond ((>= y x) z)
+         (t (tak21 (tak77 (- x 1) y z)
+                   (tak31 (- y 1) z x)
+                   (tak57 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak21))
+(defun tak21 (x y z)
+   (cond ((>= y x) z)
+         (t (tak22 (tak14 (- x 1) y z)
+                   (tak42 (- y 1) z x)
+                   (tak74 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak22))
+(defun tak22 (x y z)
+   (cond ((>= y x) z)
+         (t (tak23 (tak51 (- x 1) y z)
+                   (tak53 (- y 1) z x)
+                   (tak91 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak23))
+(defun tak23 (x y z)
+   (cond ((>= y x) z)
+         (t (tak24 (tak88 (- x 1) y z)
+                   (tak64 (- y 1) z x)
+                   (tak8 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak24))
+(defun tak24 (x y z)
+   (cond ((>= y x) z)
+         (t (tak25 (tak25 (- x 1) y z)
+                   (tak75 (- y 1) z x)
+                   (tak25 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak25))
+(defun tak25 (x y z)
+   (cond ((>= y x) z)
+         (t (tak26 (tak62 (- x 1) y z)
+                   (tak86 (- y 1) z x)
+                   (tak42 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak26))
+(defun tak26 (x y z)
+   (cond ((>= y x) z)
+         (t (tak27 (tak99 (- x 1) y z)
+                   (tak97 (- y 1) z x)
+                   (tak59 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak27))
+(defun tak27 (x y z)
+   (cond ((>= y x) z)
+         (t (tak28 (tak36 (- x 1) y z)
+                   (tak8 (- y 1) z x)
+                   (tak76 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak28))
+(defun tak28 (x y z)
+   (cond ((>= y x) z)
+         (t (tak29 (tak73 (- x 1) y z)
+                   (tak19 (- y 1) z x)
+                   (tak93 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak29))
+(defun tak29 (x y z)
+   (cond ((>= y x) z)
+         (t (tak30 (tak10 (- x 1) y z)
+                   (tak30 (- y 1) z x)
+                   (tak10 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak30))
+(defun tak30 (x y z)
+   (cond ((>= y x) z)
+         (t (tak31 (tak47 (- x 1) y z)
+                   (tak41 (- y 1) z x)
+                   (tak27 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak31))
+(defun tak31 (x y z)
+   (cond ((>= y x) z)
+         (t (tak32 (tak84 (- x 1) y z)
+                   (tak52 (- y 1) z x)
+                   (tak44 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak32))
+(defun tak32 (x y z)
+   (cond ((>= y x) z)
+         (t (tak33 (tak21 (- x 1) y z)
+                   (tak63 (- y 1) z x)
+                   (tak61 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak33))
+(defun tak33 (x y z)
+   (cond ((>= y x) z)
+         (t (tak34 (tak58 (- x 1) y z)
+                   (tak74 (- y 1) z x)
+                   (tak78 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak34))
+(defun tak34 (x y z)
+   (cond ((>= y x) z)
+         (t (tak35 (tak95 (- x 1) y z)
+                   (tak85 (- y 1) z x)
+                   (tak95 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak35))
+(defun tak35 (x y z)
+   (cond ((>= y x) z)
+         (t (tak36 (tak32 (- x 1) y z)
+                   (tak96 (- y 1) z x)
+                   (tak12 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak36))
+(defun tak36 (x y z)
+   (cond ((>= y x) z)
+         (t (tak37 (tak69 (- x 1) y z)
+                   (tak7 (- y 1) z x)
+                   (tak29 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak37))
+(defun tak37 (x y z)
+   (cond ((>= y x) z)
+         (t (tak38 (tak6 (- x 1) y z)
+                   (tak18 (- y 1) z x)
+                   (tak46 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak38))
+(defun tak38 (x y z)
+   (cond ((>= y x) z)
+         (t (tak39 (tak43 (- x 1) y z)
+                   (tak29 (- y 1) z x)
+                   (tak63 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak39))
+(defun tak39 (x y z)
+   (cond ((>= y x) z)
+         (t (tak40 (tak80 (- x 1) y z)
+                   (tak40 (- y 1) z x)
+                   (tak80 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak40))
+(defun tak40 (x y z)
+   (cond ((>= y x) z)
+         (t (tak41 (tak17 (- x 1) y z)
+                   (tak51 (- y 1) z x)
+                   (tak97 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak41))
+(defun tak41 (x y z)
+   (cond ((>= y x) z)
+         (t (tak42 (tak54 (- x 1) y z)
+                   (tak62 (- y 1) z x)
+                   (tak14 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak42))
+(defun tak42 (x y z)
+   (cond ((>= y x) z)
+         (t (tak43 (tak91 (- x 1) y z)
+                   (tak73 (- y 1) z x)
+                   (tak31 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak43))
+(defun tak43 (x y z)
+   (cond ((>= y x) z)
+         (t (tak44 (tak28 (- x 1) y z)
+                   (tak84 (- y 1) z x)
+                   (tak48 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak44))
+(defun tak44 (x y z)
+   (cond ((>= y x) z)
+         (t (tak45 (tak65 (- x 1) y z)
+                   (tak95 (- y 1) z x)
+                   (tak65 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak45))
+(defun tak45 (x y z)
+   (cond ((>= y x) z)
+         (t (tak46 (tak2 (- x 1) y z)
+                   (tak6 (- y 1) z x)
+                   (tak82 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak46))
+(defun tak46 (x y z)
+   (cond ((>= y x) z)
+         (t (tak47 (tak39 (- x 1) y z)
+                   (tak17 (- y 1) z x)
+                   (tak99 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak47))
+(defun tak47 (x y z)
+   (cond ((>= y x) z)
+         (t (tak48 (tak76 (- x 1) y z)
+                   (tak28 (- y 1) z x)
+                   (tak16 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak48))
+(defun tak48 (x y z)
+   (cond ((>= y x) z)
+         (t (tak49 (tak13 (- x 1) y z)
+                   (tak39 (- y 1) z x)
+                   (tak33 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak49))
+(defun tak49 (x y z)
+   (cond ((>= y x) z)
+         (t (tak50 (tak50 (- x 1) y z)
+                   (tak50 (- y 1) z x)
+                   (tak50 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak50))
+(defun tak50 (x y z)
+   (cond ((>= y x) z)
+         (t (tak51 (tak87 (- x 1) y z)
+                   (tak61 (- y 1) z x)
+                   (tak67 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak51))
+(defun tak51 (x y z)
+   (cond ((>= y x) z)
+         (t (tak52 (tak24 (- x 1) y z)
+                   (tak72 (- y 1) z x)
+                   (tak84 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak52))
+(defun tak52 (x y z)
+   (cond ((>= y x) z)
+         (t (tak53 (tak61 (- x 1) y z)
+                   (tak83 (- y 1) z x)
+                   (tak1 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak53))
+(defun tak53 (x y z)
+   (cond ((>= y x) z)
+         (t (tak54 (tak98 (- x 1) y z)
+                   (tak94 (- y 1) z x)
+                   (tak18 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak54))
+(defun tak54 (x y z)
+   (cond ((>= y x) z)
+         (t (tak55 (tak35 (- x 1) y z)
+                   (tak5 (- y 1) z x)
+                   (tak35 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak55))
+(defun tak55 (x y z)
+   (cond ((>= y x) z)
+         (t (tak56 (tak72 (- x 1) y z)
+                   (tak16 (- y 1) z x)
+                   (tak52 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak56))
+(defun tak56 (x y z)
+   (cond ((>= y x) z)
+         (t (tak57 (tak9 (- x 1) y z)
+                   (tak27 (- y 1) z x)
+                   (tak69 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak57))
+(defun tak57 (x y z)
+   (cond ((>= y x) z)
+         (t (tak58 (tak46 (- x 1) y z)
+                   (tak38 (- y 1) z x)
+                   (tak86 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak58))
+(defun tak58 (x y z)
+   (cond ((>= y x) z)
+         (t (tak59 (tak83 (- x 1) y z)
+                   (tak49 (- y 1) z x)
+                   (tak3 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak59))
+(defun tak59 (x y z)
+   (cond ((>= y x) z)
+         (t (tak60 (tak20 (- x 1) y z)
+                   (tak60 (- y 1) z x)
+                   (tak20 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak60))
+(defun tak60 (x y z)
+   (cond ((>= y x) z)
+         (t (tak61 (tak57 (- x 1) y z)
+                   (tak71 (- y 1) z x)
+                   (tak37 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak61))
+(defun tak61 (x y z)
+   (cond ((>= y x) z)
+         (t (tak62 (tak94 (- x 1) y z)
+                   (tak82 (- y 1) z x)
+                   (tak54 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak62))
+(defun tak62 (x y z)
+   (cond ((>= y x) z)
+         (t (tak63 (tak31 (- x 1) y z)
+                   (tak93 (- y 1) z x)
+                   (tak71 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak63))
+(defun tak63 (x y z)
+   (cond ((>= y x) z)
+         (t (tak64 (tak68 (- x 1) y z)
+                   (tak4 (- y 1) z x)
+                   (tak88 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak64))
+(defun tak64 (x y z)
+   (cond ((>= y x) z)
+         (t (tak65 (tak5 (- x 1) y z)
+                   (tak15 (- y 1) z x)
+                   (tak5 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak65))
+(defun tak65 (x y z)
+   (cond ((>= y x) z)
+         (t (tak66 (tak42 (- x 1) y z)
+                   (tak26 (- y 1) z x)
+                   (tak22 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak66))
+(defun tak66 (x y z)
+   (cond ((>= y x) z)
+         (t (tak67 (tak79 (- x 1) y z)
+                   (tak37 (- y 1) z x)
+                   (tak39 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak67))
+(defun tak67 (x y z)
+   (cond ((>= y x) z)
+         (t (tak68 (tak16 (- x 1) y z)
+                   (tak48 (- y 1) z x)
+                   (tak56 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak68))
+(defun tak68 (x y z)
+   (cond ((>= y x) z)
+         (t (tak69 (tak53 (- x 1) y z)
+                   (tak59 (- y 1) z x)
+                   (tak73 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak69))
+(defun tak69 (x y z)
+   (cond ((>= y x) z)
+         (t (tak70 (tak90 (- x 1) y z)
+                   (tak70 (- y 1) z x)
+                   (tak90 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak70))
+(defun tak70 (x y z)
+   (cond ((>= y x) z)
+         (t (tak71 (tak27 (- x 1) y z)
+                   (tak81 (- y 1) z x)
+                   (tak7 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak71))
+(defun tak71 (x y z)
+   (cond ((>= y x) z)
+         (t (tak72 (tak64 (- x 1) y z)
+                   (tak92 (- y 1) z x)
+                   (tak24 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak72))
+(defun tak72 (x y z)
+   (cond ((>= y x) z)
+         (t (tak73 (tak1 (- x 1) y z)
+                   (tak3 (- y 1) z x)
+                   (tak41 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak73))
+(defun tak73 (x y z)
+   (cond ((>= y x) z)
+         (t (tak74 (tak38 (- x 1) y z)
+                   (tak14 (- y 1) z x)
+                   (tak58 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak74))
+(defun tak74 (x y z)
+   (cond ((>= y x) z)
+         (t (tak75 (tak75 (- x 1) y z)
+                   (tak25 (- y 1) z x)
+                   (tak75 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak75))
+(defun tak75 (x y z)
+   (cond ((>= y x) z)
+         (t (tak76 (tak12 (- x 1) y z)
+                   (tak36 (- y 1) z x)
+                   (tak92 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak76))
+(defun tak76 (x y z)
+   (cond ((>= y x) z)
+         (t (tak77 (tak49 (- x 1) y z)
+                   (tak47 (- y 1) z x)
+                   (tak9 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak77))
+(defun tak77 (x y z)
+   (cond ((>= y x) z)
+         (t (tak78 (tak86 (- x 1) y z)
+                   (tak58 (- y 1) z x)
+                   (tak26 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak78))
+(defun tak78 (x y z)
+   (cond ((>= y x) z)
+         (t (tak79 (tak23 (- x 1) y z)
+                   (tak69 (- y 1) z x)
+                   (tak43 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak79))
+(defun tak79 (x y z)
+   (cond ((>= y x) z)
+         (t (tak80 (tak60 (- x 1) y z)
+                   (tak80 (- y 1) z x)
+                   (tak60 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak80))
+(defun tak80 (x y z)
+  (cond ((>= y x) z)
+        (t (tak81 (tak97 (- x 1) y z)
+                  (tak91 (- y 1) z x)
+                  (tak77 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak81))
+(defun tak81 (x y z)
+   (cond ((>= y x) z)
+         (t (tak82 (tak34 (- x 1) y z)
+                   (tak2 (- y 1) z x)
+                   (tak94 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak82))
+(defun tak82 (x y z)
+   (cond ((>= y x) z)
+         (t (tak83 (tak71 (- x 1) y z)
+                   (tak13 (- y 1) z x)
+                   (tak11 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak83))
+(defun tak83 (x y z)
+   (cond ((>= y x) z)
+         (t (tak84 (tak8 (- x 1) y z)
+                   (tak24 (- y 1) z x)
+                   (tak28 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak84))
+(defun tak84 (x y z)
+   (cond ((>= y x) z)
+         (t (tak85 (tak45 (- x 1) y z)
+                   (tak35 (- y 1) z x)
+                   (tak45 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak85))
+(defun tak85 (x y z)
+   (cond ((>= y x) z)
+         (t (tak86 (tak82 (- x 1) y z)
+                   (tak46 (- y 1) z x)
+                   (tak62 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak86))
+(defun tak86 (x y z)
+   (cond ((>= y x) z)
+         (t (tak87 (tak19 (- x 1) y z)
+                   (tak57 (- y 1) z x)
+                   (tak79 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak87))
+(defun tak87 (x y z)
+   (cond ((>= y x) z)
+         (t (tak88 (tak56 (- x 1) y z)
+                   (tak68 (- y 1) z x)
+                   (tak96 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak88))
+(defun tak88 (x y z)
+   (cond ((>= y x) z)
+         (t (tak89 (tak93 (- x 1) y z)
+                   (tak79 (- y 1) z x)
+                   (tak13 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak89))
+(defun tak89 (x y z)
+   (cond ((>= y x) z)
+         (t (tak90 (tak30 (- x 1) y z)
+                   (tak90 (- y 1) z x)
+                   (tak30 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak91))
+(defun tak90 (x y z)
+   (cond ((>= y x) z)
+         (t (tak91 (tak67 (- x 1) y z)
+                   (tak1 (- y 1) z x)
+                   (tak47 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak92))
+(defun tak91 (x y z)
+   (cond ((>= y x) z)
+         (t (tak92 (tak4 (- x 1) y z)
+                   (tak12 (- y 1) z x)
+                   (tak64 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak93))
+(defun tak92 (x y z)
+   (cond ((>= y x) z)
+         (t (tak93 (tak41 (- x 1) y z)
+                   (tak23 (- y 1) z x)
+                   (tak81 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak94))
+(defun tak93 (x y z)
+   (cond ((>= y x) z)
+         (t (tak94 (tak78 (- x 1) y z)
+                   (tak34 (- y 1) z x)
+                   (tak98 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak95))
+(defun tak94 (x y z)
+   (cond ((>= y x) z)
+         (t (tak95 (tak15 (- x 1) y z)
+                   (tak45 (- y 1) z x)
+                   (tak15 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak96))
+(defun tak95 (x y z)
+   (cond ((>= y x) z)
+         (t (tak96 (tak52 (- x 1) y z)
+                   (tak56 (- y 1) z x)
+                   (tak32 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak96))
+(defun tak96 (x y z)
+   (cond ((>= y x) z)
+         (t (tak97 (tak89 (- x 1) y z)
+                   (tak67 (- y 1) z x)
+                   (tak49 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak97))
+(defun tak97 (x y z)
+   (cond ((>= y x) z)
+         (t (tak98 (tak26 (- x 1) y z)
+                   (tak78 (- y 1) z x)
+                   (tak66 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak98))
+(defun tak98 (x y z)
+   (cond ((>= y x) z)
+        (t (tak99 (tak63 (- x 1) y z)
+                  (tak89 (- y 1) z x)
+                  (tak83 (- z 1) x y)))))
+
+(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tak99))
+(defun tak99 (x y z)
+  (cond ((>= y x) z)
+        (t (lisp-takr (lisp-takr (- x 1) y z)
+                      (lisp-takr (- y 1) z x)
+                      (lisp-takr (- z 1) x y)))))
+
+;;;
+;;;
+;;;
+
+
+(cl:in-package #:coalton-benchmarks/native)
+
+(cl:declaim (cl:optimize (cl:speed 3) (cl:safety 0)))
+
+(coalton-toplevel
+
+  (declare takr (UFix -> UFix -> UFix -> UFix))
+  (define (takr x y z)
+    (cond ((>= y x) z)
+          (True (tak1 (tak37 (- x 1) y z)
+                      (tak11 (- y 1) z x)
+                      (tak17 (- z 1) x y)))))
+  
+  (declare tak1 (UFix -> UFix -> UFix -> UFix))
+  (define (tak1 x y z)
+    (cond ((>= y x) z)
+          (True (tak2 (tak74 (- x 1) y z)
+                      (tak22 (- y 1) z x)
+                      (tak34 (- z 1) x y)))))
+
+  (declare tak2 (UFix -> UFix -> UFix -> UFix))
+  (define (tak2 x y z)
+    (cond ((>= y x) z)
+          (True (tak3 (tak11 (- x 1) y z)
+                      (tak33 (- y 1) z x)
+                      (tak51 (- z 1) x y)))))
+
+  (declare tak3 (UFix -> UFix -> UFix -> UFix))
+  (define (tak3 x y z)
+    (cond ((>= y x) z)
+          (True (tak4 (tak48 (- x 1) y z)
+                      (tak44 (- y 1) z x)
+                      (tak68 (- z 1) x y)))))
+
+  (declare tak4 (UFix -> UFix -> UFix -> UFix))
+  (define (tak4 x y z)
+    (cond ((>= y x) z)
+          (True (tak5 (tak85 (- x 1) y z)
+                      (tak55 (- y 1) z x)
+                      (tak85 (- z 1) x y)))))
+
+  (declare tak5 (UFix -> UFix -> UFix -> UFix))
+  (define (tak5 x y z)
+    (cond ((>= y x) z)
+          (True (tak6 (tak22 (- x 1) y z)
+                      (tak66 (- y 1) z x)
+                      (tak2 (- z 1) x y)))))
+
+  (declare tak6 (UFix -> UFix -> UFix -> UFix))
+  (define (tak6 x y z)
+    (cond ((>= y x) z)
+          (True (tak7 (tak59 (- x 1) y z)
+                      (tak77 (- y 1) z x)
+                      (tak19 (- z 1) x y)))))
+
+  (declare tak7 (UFix -> UFix -> UFix -> UFix))
+  (define (tak7 x y z)
+    (cond ((>= y x) z)
+          (True (tak8 (tak96 (- x 1) y z)
+                      (tak88 (- y 1) z x)
+                      (tak36 (- z 1) x y)))))
+
+  (declare tak8 (UFix -> UFix -> UFix -> UFix))
+  (define (tak8 x y z)
+    (cond ((>= y x) z)
+          (True (tak9 (tak33 (- x 1) y z)
+                      (tak99 (- y 1) z x)
+                      (tak53 (- z 1) x y)))))
+
+  (declare tak9 (UFix -> UFix -> UFix -> UFix))
+  (define (tak9 x y z)
+    (cond ((>= y x) z)
+          (True (tak10 (tak70 (- x 1) y z)
+                       (tak10 (- y 1) z x)
+                       (tak70 (- z 1) x y)))))
+
+  (declare tak10 (UFix -> UFix -> UFix -> UFix))
+  (define (tak10 x y z)
+    (cond ((>= y x) z)
+          (True (tak11 (tak7 (- x 1) y z)
+                       (tak21 (- y 1) z x)
+                       (tak87 (- z 1) x y)))))
+
+  (declare tak11 (UFix -> UFix -> UFix -> UFix))
+  (define (tak11 x y z)
+    (cond ((>= y x) z)
+          (True (tak12 (tak44 (- x 1) y z)
+                       (tak32 (- y 1) z x)
+                       (tak4 (- z 1) x y)))))
+  
+  (declare tak12 (UFix -> UFix -> UFix -> UFix))
+  (define (tak12 x y z)
+    (cond ((>= y x) z)
+          (True (tak13 (tak81 (- x 1) y z)
+                       (tak43 (- y 1) z x)
+                       (tak21 (- z 1) x y)))))
+
+  (declare tak13 (UFix -> UFix -> UFix -> UFix))
+  (define (tak13 x y z)
+    (cond ((>= y x) z)
+          (True (tak14 (tak18 (- x 1) y z)
+                       (tak54 (- y 1) z x)
+                       (tak38 (- z 1) x y)))))
+  
+  (declare tak14 (UFix -> UFix -> UFix -> UFix))
+  (define (tak14 x y z)
+    (cond ((>= y x) z)
+          (True (tak15 (tak55 (- x 1) y z)
+                       (tak65 (- y 1) z x)
+                       (tak55 (- z 1) x y)))))
+    
+  (declare tak15 (UFix -> UFix -> UFix -> UFix))
+  (define (tak15 x y z)
+    (cond ((>= y x) z)
+          (True (tak16 (tak92 (- x 1) y z)
+                       (tak76 (- y 1) z x)
+                       (tak72 (- z 1) x y)))))
+  
+  (declare tak16 (UFix -> UFix -> UFix -> UFix))
+  (define (tak16 x y z)
+    (cond ((>= y x) z)
+          (True (tak17 (tak29 (- x 1) y z)
+                       (tak87 (- y 1) z x)
+                       (tak89 (- z 1) x y)))))
+    
+  (declare tak17 (UFix -> UFix -> UFix -> UFix))
+  (define (tak17 x y z)
+    (cond ((>= y x) z)
+          (True (tak18 (tak66 (- x 1) y z)
+                       (tak98 (- y 1) z x)
+                       (tak6 (- z 1) x y)))))
+    
+  (declare tak18 (UFix -> UFix -> UFix -> UFix))
+  (define (tak18 x y z)
+    (cond ((>= y x) z)
+          (True (tak19 (tak3 (- x 1) y z)
+                       (tak9 (- y 1) z x)
+                       (tak23 (- z 1) x y)))))
+    
+  (declare tak19 (UFix -> UFix -> UFix -> UFix))
+  (define (tak19 x y z)
+    (cond ((>= y x) z)
+          (True (tak20 (tak40 (- x 1) y z)
+                       (tak20 (- y 1) z x)
+                       (tak40 (- z 1) x y)))))
+  
+  (declare tak20 (UFix -> UFix -> UFix -> UFix))
+  (define (tak20 x y z)
+    (cond ((>= y x) z)
+          (True (tak21 (tak77 (- x 1) y z)
+                       (tak31 (- y 1) z x)
+                       (tak57 (- z 1) x y)))))
+  
+  (declare tak21 (UFix -> UFix -> UFix -> UFix))
+  (define (tak21 x y z)
+    (cond ((>= y x) z)
+          (True (tak22 (tak14 (- x 1) y z)
+                       (tak42 (- y 1) z x)
+                       (tak74 (- z 1) x y)))))
+    
+  (declare tak22 (UFix -> UFix -> UFix -> UFix))
+  (define (tak22 x y z)
+    (cond ((>= y x) z)
+          (True (tak23 (tak51 (- x 1) y z)
+                       (tak53 (- y 1) z x)
+                       (tak91 (- z 1) x y)))))
+    
+  (declare tak23 (UFix -> UFix -> UFix -> UFix))
+  (define (tak23 x y z)
+    (cond ((>= y x) z)
+          (True (tak24 (tak88 (- x 1) y z)
+                       (tak64 (- y 1) z x)
+                       (tak8 (- z 1) x y)))))
+    
+  (declare tak24 (UFix -> UFix -> UFix -> UFix))
+  (define (tak24 x y z)
+    (cond ((>= y x) z)
+          (True (tak25 (tak25 (- x 1) y z)
+                       (tak75 (- y 1) z x)
+                       (tak25 (- z 1) x y)))))
+    
+  (declare tak25 (UFix -> UFix -> UFix -> UFix))
+  (define (tak25 x y z)
+    (cond ((>= y x) z)
+          (True (tak26 (tak62 (- x 1) y z)
+                       (tak86 (- y 1) z x)
+                       (tak42 (- z 1) x y)))))
+    
+  (declare tak26 (UFix -> UFix -> UFix -> UFix))
+  (define (tak26 x y z)
+    (cond ((>= y x) z)
+          (True (tak27 (tak99 (- x 1) y z)
+                       (tak97 (- y 1) z x)
+                       (tak59 (- z 1) x y)))))
+    
+  (declare tak27 (UFix -> UFix -> UFix -> UFix))
+  (define (tak27 x y z)
+    (cond ((>= y x) z)
+          (True (tak28 (tak36 (- x 1) y z)
+                       (tak8 (- y 1) z x)
+                       (tak76 (- z 1) x y)))))
+    
+  (declare tak28 (UFix -> UFix -> UFix -> UFix))
+  (define (tak28 x y z)
+    (cond ((>= y x) z)
+          (True (tak29 (tak73 (- x 1) y z)
+                       (tak19 (- y 1) z x)
+                       (tak93 (- z 1) x y)))))
+    
+  (declare tak29 (UFix -> UFix -> UFix -> UFix))
+  (define (tak29 x y z)
+    (cond ((>= y x) z)
+          (True (tak30 (tak10 (- x 1) y z)
+                       (tak30 (- y 1) z x)
+                       (tak10 (- z 1) x y)))))
+    
+  (declare tak30 (UFix -> UFix -> UFix -> UFix))
+  (define (tak30 x y z)
+    (cond ((>= y x) z)
+          (True (tak31 (tak47 (- x 1) y z)
+                       (tak41 (- y 1) z x)
+                       (tak27 (- z 1) x y)))))
+    
+  (declare tak31 (UFix -> UFix -> UFix -> UFix))
+  (define (tak31 x y z)
+    (cond ((>= y x) z)
+          (True (tak32 (tak84 (- x 1) y z)
+                       (tak52 (- y 1) z x)
+                       (tak44 (- z 1) x y)))))
+    
+  (declare tak32 (UFix -> UFix -> UFix -> UFix))
+  (define (tak32 x y z)
+    (cond ((>= y x) z)
+          (True (tak33 (tak21 (- x 1) y z)
+                       (tak63 (- y 1) z x)
+                       (tak61 (- z 1) x y)))))
+      
+  (declare tak33 (UFix -> UFix -> UFix -> UFix))
+  (define (tak33 x y z)
+    (cond ((>= y x) z)
+          (True (tak34 (tak58 (- x 1) y z)
+                       (tak74 (- y 1) z x)
+                       (tak78 (- z 1) x y)))))
+      
+  (declare tak34 (UFix -> UFix -> UFix -> UFix))
+  (define (tak34 x y z)
+    (cond ((>= y x) z)
+          (True (tak35 (tak95 (- x 1) y z)
+                       (tak85 (- y 1) z x)
+                       (tak95 (- z 1) x y)))))
+      
+  (declare tak35 (UFix -> UFix -> UFix -> UFix))
+  (define (tak35 x y z)
+    (cond ((>= y x) z)
+          (True (tak36 (tak32 (- x 1) y z)
+                       (tak96 (- y 1) z x)
+                       (tak12 (- z 1) x y)))))
+      
+  (declare tak36 (UFix -> UFix -> UFix -> UFix))
+  (define (tak36 x y z)
+    (cond ((>= y x) z)
+          (True (tak37 (tak69 (- x 1) y z)
+                       (tak7 (- y 1) z x)
+                       (tak29 (- z 1) x y)))))
+      
+  (declare tak37 (UFix -> UFix -> UFix -> UFix))
+  (define (tak37 x y z)
+    (cond ((>= y x) z)
+          (True (tak38 (tak6 (- x 1) y z)
+                       (tak18 (- y 1) z x)
+                       (tak46 (- z 1) x y)))))
+      
+  (declare tak38 (UFix -> UFix -> UFix -> UFix))
+  (define (tak38 x y z)
+    (cond ((>= y x) z)
+          (True (tak39 (tak43 (- x 1) y z)
+                       (tak29 (- y 1) z x)
+                       (tak63 (- z 1) x y)))))
+      
+  (declare tak39 (UFix -> UFix -> UFix -> UFix))
+  (define (tak39 x y z)
+    (cond ((>= y x) z)
+          (True (tak40 (tak80 (- x 1) y z)
+                       (tak40 (- y 1) z x)
+                       (tak80 (- z 1) x y)))))
+      
+  (declare tak40 (UFix -> UFix -> UFix -> UFix))
+  (define (tak40 x y z)
+    (cond ((>= y x) z)
+          (True (tak41 (tak17 (- x 1) y z)
+                       (tak51 (- y 1) z x)
+                       (tak97 (- z 1) x y)))))
+      
+  (declare tak41 (UFix -> UFix -> UFix -> UFix))
+  (define (tak41 x y z)
+    (cond ((>= y x) z)
+          (True (tak42 (tak54 (- x 1) y z)
+                       (tak62 (- y 1) z x)
+                       (tak14 (- z 1) x y)))))
+        
+  (declare tak42 (UFix -> UFix -> UFix -> UFix))
+  (define (tak42 x y z)
+    (cond ((>= y x) z)
+          (True (tak43 (tak91 (- x 1) y z)
+                       (tak73 (- y 1) z x)
+                       (tak31 (- z 1) x y)))))
+        
+  (declare tak43 (UFix -> UFix -> UFix -> UFix))
+  (define (tak43 x y z)
+    (cond ((>= y x) z)
+          (True (tak44 (tak28 (- x 1) y z)
+                       (tak84 (- y 1) z x)
+                       (tak48 (- z 1) x y)))))
+        
+  (declare tak44 (UFix -> UFix -> UFix -> UFix))
+  (define (tak44 x y z)
+    (cond ((>= y x) z)
+          (True (tak45 (tak65 (- x 1) y z)
+                       (tak95 (- y 1) z x)
+                       (tak65 (- z 1) x y)))))
+        
+  (declare tak45 (UFix -> UFix -> UFix -> UFix))
+  (define (tak45 x y z)
+    (cond ((>= y x) z)
+          (True (tak46 (tak2 (- x 1) y z)
+                       (tak6 (- y 1) z x)
+                       (tak82 (- z 1) x y)))))
+        
+  (declare tak46 (UFix -> UFix -> UFix -> UFix))
+  (define (tak46 x y z)
+    (cond ((>= y x) z)
+          (True (tak47 (tak39 (- x 1) y z)
+                       (tak17 (- y 1) z x)
+                       (tak99 (- z 1) x y)))))
+        
+  (declare tak47 (UFix -> UFix -> UFix -> UFix))
+  (define (tak47 x y z)
+    (cond ((>= y x) z)
+          (True (tak48 (tak76 (- x 1) y z)
+                       (tak28 (- y 1) z x)
+                       (tak16 (- z 1) x y)))))
+        
+  (declare tak48 (UFix -> UFix -> UFix -> UFix))
+  (define (tak48 x y z)
+    (cond ((>= y x) z)
+          (True (tak49 (tak13 (- x 1) y z)
+                       (tak39 (- y 1) z x)
+                       (tak33 (- z 1) x y)))))
+        
+  (declare tak49 (UFix -> UFix -> UFix -> UFix))
+  (define (tak49 x y z)
+    (cond ((>= y x) z)
+          (True (tak50 (tak50 (- x 1) y z)
+                       (tak50 (- y 1) z x)
+                       (tak50 (- z 1) x y)))))
+        
+  (declare tak50 (UFix -> UFix -> UFix -> UFix))
+  (define (tak50 x y z)
+    (cond ((>= y x) z)
+          (True (tak51 (tak87 (- x 1) y z)
+                       (tak61 (- y 1) z x)
+                       (tak67 (- z 1) x y)))))
+          
+  (declare tak51 (UFix -> UFix -> UFix -> UFix))
+  (define (tak51 x y z)
+    (cond ((>= y x) z)
+          (True (tak52 (tak24 (- x 1) y z)
+                       (tak72 (- y 1) z x)
+                       (tak84 (- z 1) x y)))))
+          
+  (declare tak52 (UFix -> UFix -> UFix -> UFix))
+  (define (tak52 x y z)
+    (cond ((>= y x) z)
+          (True (tak53 (tak61 (- x 1) y z)
+                       (tak83 (- y 1) z x)
+                       (tak1 (- z 1) x y)))))
+          
+  (declare tak53 (UFix -> UFix -> UFix -> UFix))
+  (define (tak53 x y z)
+    (cond ((>= y x) z)
+          (True (tak54 (tak98 (- x 1) y z)
+                       (tak94 (- y 1) z x)
+                       (tak18 (- z 1) x y)))))
+          
+  (declare tak54 (UFix -> UFix -> UFix -> UFix))
+  (define (tak54 x y z)
+    (cond ((>= y x) z)
+          (True (tak55 (tak35 (- x 1) y z)
+                       (tak5 (- y 1) z x)
+                       (tak35 (- z 1) x y)))))
+          
+  (declare tak55 (UFix -> UFix -> UFix -> UFix))
+  (define (tak55 x y z)
+    (cond ((>= y x) z)
+          (True (tak56 (tak72 (- x 1) y z)
+                       (tak16 (- y 1) z x)
+                       (tak52 (- z 1) x y)))))
+          
+  (declare tak56 (UFix -> UFix -> UFix -> UFix))
+  (define (tak56 x y z)
+    (cond ((>= y x) z)
+          (True (tak57 (tak9 (- x 1) y z)
+                       (tak27 (- y 1) z x)
+                       (tak69 (- z 1) x y)))))
+          
+  (declare tak57 (UFix -> UFix -> UFix -> UFix))
+  (define (tak57 x y z)
+    (cond ((>= y x) z)
+          (True (tak58 (tak46 (- x 1) y z)
+                       (tak38 (- y 1) z x)
+                       (tak86 (- z 1) x y)))))
+          
+  (declare tak58 (UFix -> UFix -> UFix -> UFix))
+  (define (tak58 x y z)
+    (cond ((>= y x) z)
+          (True (tak59 (tak83 (- x 1) y z)
+                       (tak49 (- y 1) z x)
+                       (tak3 (- z 1) x y)))))
+          
+  (declare tak59 (UFix -> UFix -> UFix -> UFix))
+  (define (tak59 x y z)
+    (cond ((>= y x) z)
+          (True (tak60 (tak20 (- x 1) y z)
+                       (tak60 (- y 1) z x)
+                       (tak20 (- z 1) x y)))))
+          
+  (declare tak60 (UFix -> UFix -> UFix -> UFix))
+  (define (tak60 x y z)
+    (cond ((>= y x) z)
+          (True (tak61 (tak57 (- x 1) y z)
+                       (tak71 (- y 1) z x)
+                       (tak37 (- z 1) x y)))))
+            
+  (declare tak61 (UFix -> UFix -> UFix -> UFix))
+  (define (tak61 x y z)
+    (cond ((>= y x) z)
+          (True (tak62 (tak94 (- x 1) y z)
+                       (tak82 (- y 1) z x)
+                       (tak54 (- z 1) x y)))))
+            
+  (declare tak62 (UFix -> UFix -> UFix -> UFix))
+  (define (tak62 x y z)
+    (cond ((>= y x) z)
+          (True (tak63 (tak31 (- x 1) y z)
+                       (tak93 (- y 1) z x)
+                       (tak71 (- z 1) x y)))))
+            
+  (declare tak63 (UFix -> UFix -> UFix -> UFix))
+  (define (tak63 x y z)
+    (cond ((>= y x) z)
+          (True (tak64 (tak68 (- x 1) y z)
+                       (tak4 (- y 1) z x)
+                       (tak88 (- z 1) x y)))))
+            
+  (declare tak64 (UFix -> UFix -> UFix -> UFix))
+  (define (tak64 x y z)
+    (cond ((>= y x) z)
+          (True (tak65 (tak5 (- x 1) y z)
+                       (tak15 (- y 1) z x)
+                       (tak5 (- z 1) x y)))))
+            
+  (declare tak65 (UFix -> UFix -> UFix -> UFix))
+  (define (tak65 x y z)
+    (cond ((>= y x) z)
+          (True (tak66 (tak42 (- x 1) y z)
+                       (tak26 (- y 1) z x)
+                       (tak22 (- z 1) x y)))))
+            
+  (declare tak66 (UFix -> UFix -> UFix -> UFix))
+  (define (tak66 x y z)
+    (cond ((>= y x) z)
+          (True (tak67 (tak79 (- x 1) y z)
+                       (tak37 (- y 1) z x)
+                       (tak39 (- z 1) x y)))))
+            
+  (declare tak67 (UFix -> UFix -> UFix -> UFix))
+  (define (tak67 x y z)
+    (cond ((>= y x) z)
+          (True (tak68 (tak16 (- x 1) y z)
+                       (tak48 (- y 1) z x)
+                       (tak56 (- z 1) x y)))))
+            
+  (declare tak68 (UFix -> UFix -> UFix -> UFix))
+  (define (tak68 x y z)
+    (cond ((>= y x) z)
+          (True (tak69 (tak53 (- x 1) y z)
+                       (tak59 (- y 1) z x)
+                       (tak73 (- z 1) x y)))))
+            
+  (declare tak69 (UFix -> UFix -> UFix -> UFix))
+  (define (tak69 x y z)
+    (cond ((>= y x) z)
+          (True (tak70 (tak90 (- x 1) y z)
+                       (tak70 (- y 1) z x)
+                       (tak90 (- z 1) x y)))))
+            
+  (declare tak70 (UFix -> UFix -> UFix -> UFix))
+  (define (tak70 x y z)
+    (cond ((>= y x) z)
+          (True (tak71 (tak27 (- x 1) y z)
+                       (tak81 (- y 1) z x)
+                       (tak7 (- z 1) x y)))))
+            
+  (declare tak71 (UFix -> UFix -> UFix -> UFix))
+  (define (tak71 x y z)
+    (cond ((>= y x) z)
+          (True (tak72 (tak64 (- x 1) y z)
+                       (tak92 (- y 1) z x)
+                       (tak24 (- z 1) x y)))))
+              
+  (declare tak72 (UFix -> UFix -> UFix -> UFix))
+  (define (tak72 x y z)
+    (cond ((>= y x) z)
+          (True (tak73 (tak1 (- x 1) y z)
+                       (tak3 (- y 1) z x)
+                       (tak41 (- z 1) x y)))))
+              
+  (declare tak73 (UFix -> UFix -> UFix -> UFix))
+  (define (tak73 x y z)
+    (cond ((>= y x) z)
+          (True (tak74 (tak38 (- x 1) y z)
+                       (tak14 (- y 1) z x)
+                       (tak58 (- z 1) x y)))))
+              
+  (declare tak74 (UFix -> UFix -> UFix -> UFix))
+  (define (tak74 x y z)
+    (cond ((>= y x) z)
+          (True (tak75 (tak75 (- x 1) y z)
+                       (tak25 (- y 1) z x)
+                       (tak75 (- z 1) x y)))))
+              
+  (declare tak75 (UFix -> UFix -> UFix -> UFix))
+  (define (tak75 x y z)
+    (cond ((>= y x) z)
+          (True (tak76 (tak12 (- x 1) y z)
+                       (tak36 (- y 1) z x)
+                       (tak92 (- z 1) x y)))))
+              
+  (declare tak76 (UFix -> UFix -> UFix -> UFix))
+  (define (tak76 x y z)
+    (cond ((>= y x) z)
+          (True (tak77 (tak49 (- x 1) y z)
+                       (tak47 (- y 1) z x)
+                       (tak9 (- z 1) x y)))))
+             
+  (declare tak77 (UFix -> UFix -> UFix -> UFix))
+  (define (tak77 x y z)
+    (cond ((>= y x) z)
+          (True (tak78 (tak86 (- x 1) y z)
+                       (tak58 (- y 1) z x)
+                       (tak26 (- z 1) x y)))))
+              
+  (declare tak78 (UFix -> UFix -> UFix -> UFix))
+  (define (tak78 x y z)
+    (cond ((>= y x) z)
+          (True (tak79 (tak23 (- x 1) y z)
+                       (tak69 (- y 1) z x)
+                       (tak43 (- z 1) x y)))))
+              
+  (declare tak79 (UFix -> UFix -> UFix -> UFix))
+  (define (tak79 x y z)
+    (cond ((>= y x) z)
+          (True (tak80 (tak60 (- x 1) y z)
+                       (tak80 (- y 1) z x)
+                       (tak60 (- z 1) x y)))))
+              
+  (declare tak80 (UFix -> UFix -> UFix -> UFix))
+  (define (tak80 x y z)
+    (cond ((>= y x) z)
+          (True (tak81 (tak97 (- x 1) y z)
+                       (tak91 (- y 1) z x)
+                       (tak77 (- z 1) x y)))))
+                
+  (declare tak81 (UFix -> UFix -> UFix -> UFix))
+  (define (tak81 x y z)
+    (cond ((>= y x) z)
+          (True (tak82 (tak34 (- x 1) y z)
+                       (tak2 (- y 1) z x)
+                       (tak94 (- z 1) x y)))))
+                
+  (declare tak82 (UFix -> UFix -> UFix -> UFix))
+  (define (tak82 x y z)
+    (cond ((>= y x) z)
+          (True (tak83 (tak71 (- x 1) y z)
+                       (tak13 (- y 1) z x)
+                       (tak11 (- z 1) x y)))))
+                
+  (declare tak83 (UFix -> UFix -> UFix -> UFix))
+  (define (tak83 x y z)
+    (cond ((>= y x) z)
+          (True (tak84 (tak8 (- x 1) y z)
+                       (tak24 (- y 1) z x)
+                       (tak28 (- z 1) x y)))))
+                
+  (declare tak84 (UFix -> UFix -> UFix -> UFix))
+  (define (tak84 x y z)
+    (cond ((>= y x) z)
+          (True (tak85 (tak45 (- x 1) y z)
+                       (tak35 (- y 1) z x)
+                       (tak45 (- z 1) x y)))))
+                
+  (declare tak85 (UFix -> UFix -> UFix -> UFix))
+  (define (tak85 x y z)
+    (cond ((>= y x) z)
+          (True (tak86 (tak82 (- x 1) y z)
+                       (tak46 (- y 1) z x)
+                       (tak62 (- z 1) x y)))))
+                
+  (declare tak86 (UFix -> UFix -> UFix -> UFix))
+  (define (tak86 x y z)
+    (cond ((>= y x) z)
+          (True (tak87 (tak19 (- x 1) y z)
+                       (tak57 (- y 1) z x)
+                       (tak79 (- z 1) x y)))))
+                
+  (declare tak87 (UFix -> UFix -> UFix -> UFix))
+  (define (tak87 x y z)
+    (cond ((>= y x) z)
+          (True (tak88 (tak56 (- x 1) y z)
+                       (tak68 (- y 1) z x)
+                       (tak96 (- z 1) x y)))))
+                
+  (declare tak88 (UFix -> UFix -> UFix -> UFix))
+  (define (tak88 x y z)
+    (cond ((>= y x) z)
+          (True (tak89 (tak93 (- x 1) y z)
+                       (tak79 (- y 1) z x)
+                       (tak13 (- z 1) x y)))))
+                
+  (declare tak89 (UFix -> UFix -> UFix -> UFix))
+  (define (tak89 x y z)
+    (cond ((>= y x) z)
+          (True (tak90 (tak30 (- x 1) y z)
+                       (tak90 (- y 1) z x)
+                       (tak30 (- z 1) x y)))))
+                
+  (declare tak90 (UFix -> UFix -> UFix -> UFix))
+  (define (tak90 x y z)
+    (cond ((>= y x) z)
+          (True (tak91 (tak67 (- x 1) y z)
+                       (tak1 (- y 1) z x)
+                       (tak47 (- z 1) x y)))))
+                  
+  (declare tak91 (UFix -> UFix -> UFix -> UFix))
+  (define (tak91 x y z)
+    (cond ((>= y x) z)
+          (True (tak92 (tak4 (- x 1) y z)
+                       (tak12 (- y 1) z x)
+                       (tak64 (- z 1) x y)))))
+                  
+  (declare tak92 (UFix -> UFix -> UFix -> UFix))
+    (define (tak92 x y z)
+    (cond ((>= y x) z)
+          (True (tak93 (tak41 (- x 1) y z)
+                       (tak23 (- y 1) z x)
+                       (tak81 (- z 1) x y)))))
+                    
+  (declare tak93 (UFix -> UFix -> UFix -> UFix))
+  (define (tak93 x y z)
+    (cond ((>= y x) z)
+          (True (tak94 (tak78 (- x 1) y z)
+                       (tak34 (- y 1) z x)
+                       (tak98 (- z 1) x y)))))
+                    
+  (declare tak94 (UFix -> UFix -> UFix -> UFix))
+  (define (tak94 x y z)
+    (cond ((>= y x) z)
+          (True (tak95 (tak15 (- x 1) y z)
+                       (tak45 (- y 1) z x)
+                       (tak15 (- z 1) x y)))))
+                    
+  (declare tak95 (UFix -> UFix -> UFix -> UFix))
+  (define (tak95 x y z)
+    (cond ((>= y x) z)
+          (True (tak96 (tak52 (- x 1) y z)
+                       (tak56 (- y 1) z x)
+                       (tak32 (- z 1) x y)))))
+                    
+  (declare tak96 (UFix -> UFix -> UFix -> UFix))
+  (define (tak96 x y z)
+    (cond ((>= y x) z)
+          (True (tak97 (tak89 (- x 1) y z)
+                       (tak67 (- y 1) z x)
+                       (tak49 (- z 1) x y)))))
+                    
+  (declare tak97 (UFix -> UFix -> UFix -> UFix))
+  (define (tak97 x y z)
+    (cond ((>= y x) z)
+          (True (tak98 (tak26 (- x 1) y z)
+                       (tak78 (- y 1) z x)
+                       (tak66 (- z 1) x y)))))
+                    
+  (declare tak98 (UFix -> UFix -> UFix -> UFix))
+  (define (tak98 x y z)
+    (cond ((>= y x) z)
+          (True (tak99 (tak63 (- x 1) y z)
+                       (tak89 (- y 1) z x)
+                       (tak83 (- z 1) x y)))))
+                    
+  (declare tak99 (UFix -> UFix -> UFix -> UFix))
+  (define (tak99 x y z)
+    (cond ((>= y x) z)
+          (True (takr (takr (- x 1) y z)
+                      (takr (- y 1) z x)
+                      (takr (- z 1) x y))))))
diff --git a/benchmarks/package.lisp b/benchmarks/package.lisp
index 7cbde5ffa..6e3ee4b8c 100644
--- a/benchmarks/package.lisp
+++ b/benchmarks/package.lisp
@@ -12,13 +12,21 @@
    #:coalton-prelude
    #:coalton-library/big-float
    #:coalton-library/math)
+  (:local-nicknames (#:list #:coalton-library/list))
   (:export
    #:fib
    #:fib-fixnum
    #:fib-generic-wrapped
    #:fib-monomorphized
    #:fib-generic-optional
-   #:fib-monomorphized-optional))
+   #:fib-monomorphized-optional)
+
+  ;; gabriel-benchmarks/
+  (:export
+   #:tak
+   #:stak
+   #:takl
+   #:takr))
 
 (cl:in-package #:coalton-benchmarks)
 
diff --git a/coalton.asd b/coalton.asd
index 6e137bcaf..aea57a91c 100644
--- a/coalton.asd
+++ b/coalton.asd
@@ -232,7 +232,13 @@
   :serial t
   :components ((:file "package")
                (:file "fibonacci")
-               (:file "big-float")))
+               (:file "big-float")
+               (:module "gabriel-benchmarks"
+                        :serial t
+                        :components ((:file "tak")
+                                     (:file "stak")
+                                     (:file "takl")
+                                     (:file "takr")))))
 
 ;;; we need to inspect the sbcl version in order to decide which version of the hashtable shim to load,
 ;;; because 2.1.12 includes (or will include) a bugfix that allows a cleaner, more maintainable