--- /dev/null
+{-# language LambdaCase #-}
+
+module Virtual.CAM where
+
+-- From Interpreter to Compiler and
+-- Virtual Machine: A Functional Derivation
+-- https://pdfs.semanticscholar.org/08f9/c12239dd720cb28a1039db9ce706cc7ee3b2.pdf
+
+data Term = Var Int | Lam Term | App Term Term | Nil | MkPair Term Term | Car Term | Cdr Term | Lit Int
+
+data Inst = Fst | Snd | Push | Swap | Cons | Call | Cur [Inst] | Quote Val
+ deriving (Show)
+
+data Val = Null | Pair Val Val | Closure Val [Inst] | Num Int
+ deriving (Show)
+
+type Stack = [Val]
+
+compile :: Term -> [Inst]
+compile = \case
+ (Var 0) -> [Snd]
+ (Var n) -> Fst : compile (Var $ n - 1)
+ (Lam t) -> [Cur $ compile t]
+ (App t0 t1) -> Push : compile t0 ++ (Swap : compile t1) ++ [Cons, Call]
+ Nil -> [Quote Null]
+ (MkPair t0 t1) -> Push : compile t0 ++ (Swap : compile t1) ++ [Cons]
+ (Car t) -> compile t ++ [Fst]
+ (Cdr t) -> compile t ++ [Snd]
+ (Lit n) -> [Quote $ Num n]
+
+run :: [Inst] -> Val -> Stack -> Val
+run (Fst : c) (Pair v1 _) s = run c v1 s
+run (Snd : c) (Pair _ v2) s = run c v2 s
+run (Quote v': c) _ s = run c v' s
+run (Cur c' : c) v s = run c (Closure v c') s
+run (Push : c) v s = run c v (v : s)
+run (Swap : c) v (v' : s) = run c v' (v : s)
+run (Cons : c) v (v' : s) = run c (Pair v' v) s
+run (Call : c) (Pair (Closure v c') v') s = run (c' ++ c) (Pair v v') s
+run [] v [] = v
+
+eval :: Term -> Val
+eval t = run (compile t) Null []
+
+t1 :: Term
+t1 = Car $ MkPair (Lit 1) (Lit 2)
+
+ex1 :: Val
+ex1 = eval t1
+
+--((λ 0) (λ 0)) (λ 0)
+t2 :: Term
+t2 = App (App (Lam $ Var 0) (Lam $ Var 0)) (Lam $ Var 0)
+
+ex2 :: Val
+ex2 = eval t2