gistfile1.txt

Core RedML is (so far) a one-sided, polarized L calculus in the style of Curien-Herbelin-Munch. 
Lambda calculus can be compiled to Core RedML through a bunch of gnarly macros. For instance, the term

    (((lam [x] (lam [y] (pair x y))) nil) nil)
    
should evaluate to a pair of nils. This term is compiled into Core RedML as the first stage of the following
computation trace, which shows how it computes to the desired pair.
    

State: (cut
        (μ [%12]
         (cut
          (μ [%9]
           (cut
            {(split [in x] [out %3]
              (cut
               {(split [in y] [out %5]
                 (cut
                  (μ [%6]
                   (cut x (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
                  %5))}
               %3))}
            (force {%10} (cut () (μ [%11] (cut %10 ([in %11] [out %9])))))))
          (force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out %12])))))))
        stop)
State: (cut
        (μ [%9]
         (cut
          {(split [in x] [out %3]
            (cut
             {(split [in y] [out %5]
               (cut
                (μ [%6]
                 (cut x (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
                %5))}
             %3))}
          (force {%10} (cut () (μ [%11] (cut %10 ([in %11] [out %9])))))))
        (force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out stop]))))))
State: (cut
        {(split [in x] [out %3]
          (cut
           {(split [in y] [out %5]
             (cut
              (μ [%6]
               (cut x (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
              %5))}
           %3))}
        (force {%10}
         (cut
          ()
          (μ [%11]
           (cut
            %10
            ([in %11]
             [out (force {%13}
                   (cut () (μ [%14] (cut %13 ([in %14] [out stop])))))]))))))
State: (cut
        ()
        (μ [%11]
         (cut
          (split [in x] [out %3]
           (cut
            {(split [in y] [out %5]
              (cut
               (μ [%6]
                (cut x (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
               %5))}
            %3))
          ([in %11]
           [out (force {%13}
                 (cut () (μ [%14] (cut %13 ([in %14] [out stop])))))]))))
State: (cut
        (split [in x] [out %3]
         (cut
          {(split [in y] [out %5]
            (cut
             (μ [%6]
              (cut x (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
             %5))}
          %3))
        ([in ()]
         [out (force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out stop])))))]))
State: (cut
        (split [in x] [out %3]
         (cut
          {(split [in y] [out %5]
            (cut
             (μ [%6]
              (cut x (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
             %5))}
          %3))
        ([in ()]
         [out (force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out stop])))))]))
State: (cut
        {(split [in y] [out %5]
          (cut
           (μ [%6] (cut () (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
           %5))}
        (force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out stop]))))))
State: (cut
        {(split [in y] [out %5]
          (cut
           (μ [%6] (cut () (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
           %5))}
        (force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out stop]))))))
State: (cut
        {(split [in y] [out %5]
          (cut
           (μ [%6] (cut () (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
           %5))}
        (force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out stop]))))))
State: (cut
        ()
        (μ [%14]
         (cut
          (split [in y] [out %5]
           (cut
            (μ [%6]
             (cut () (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
            %5))
          ([in %14] [out stop]))))
State: (cut
        (split [in y] [out %5]
         (cut
          (μ [%6] (cut () (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
          %5))
        ([in ()] [out stop]))
State: (cut
        (split [in y] [out %5]
         (cut
          (μ [%6] (cut () (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
          %5))
        ([in ()] [out stop]))
State: (cut
        (μ [%6] (cut () (μ [%7] (cut () (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
        stop)
State: (cut
        (μ [%6] (cut () (μ [%7] (cut () (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
        stop)
State: (cut
        (μ [%6] (cut () (μ [%7] (cut () (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
        stop)
State: (cut () (μ [%7] (cut () (μ [%8] (cut ([0 %7] [1 %8]) stop)))))
State: (cut () (μ [%8] (cut ([0 ()] [1 %8]) stop)))
State: (cut ([0 ()] [1 ()]) stop)
State: (cut ([0 ()] [1 ()]) stop)
Final: (cut ([0 ()] [1 ()]) stop)