diff --git a/bin/main.ml b/bin/main.ml
index ab20072..693aac2 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -1,77 +1,4 @@
-(* let () = print_endline "Hello, World!" *)
 open OCanren
 open Lib
-open Lam
 
-let rec substo l x a l' =
-  let open Lam in
-  conde
-    [ fresh y (l === v y) (y === x) (l' === a)
-    ; fresh
-        (m n m' n')
-        (l === app m n)
-        (l' === app m' n')
-        (substo m x a m')
-        (substo n x a n')
-    ; fresh
-        (v b)
-        (l === abs v b)
-        (conde [ x === v &&& (l' === l); fresh b' (l' === abs v b') (substo b x a b') ])
-    ]
-;;
-
-let rec evalo m n =
-  conde
-    [ fresh x (m === v x) (n === m)
-    ; fresh (x l) (m === abs x l) (n === m)
-    ; fresh
-        (f a f' a')
-        (m === app f a)
-        (evalo f f')
-        (evalo a a')
-        (conde
-           [ fresh (x l l') (f' === abs x l) (substo l x a' l') (evalo l' n)
-           ; fresh (p q) (f' === app p q) (n === app f' a')
-           ; fresh x (f' === v x) (n === app f' a')
-           ])
-    ]
-;;
-
-let a_la_quine q r s = ?&[ evalo (app q r) s; evalo (app r s) q; evalo (app s q) r ]
-
-open Tester
-
-let runL n = run_r Lam.reify (GT.show Lam.logic) n
-let run_exn eta = run_r Lam.prj_exn eta
-
-let _ =
-  run_exn (GT.show Lam.ground) 1 q qh (REPR (fun q -> substo (v varX) varX (v varY) q));
-  run_exn (GT.show Lam.ground) 1 q qh (REPR (fun q -> evalo (abs varX (v varX)) q));
-  run_exn (GT.show Lam.ground) 2 q qh (REPR (fun q -> evalo (abs varX (v varX)) q));
-  run_exn
-    (GT.show Lam.ground)
-    1
-    q
-    qh
-    (REPR (fun q -> evalo (app (abs varX (v varX)) (v varY)) q));
-  run_exn
-    (GT.show Lam.ground)
-    1
-    q
-    qh
-    (REPR (fun q -> evalo (app (abs varX (v varX)) q) (v varY)));
-  run_exn
-    (GT.show Lam.ground)
-    1
-    q
-    qh
-    (REPR (fun q -> evalo (app (abs varX q) (v varY)) (v varY)));
-  run_exn (GT.show Lam.ground) 1 q qh (REPR (fun q -> evalo (app (v varX) (v varX)) q));
-  run_exn (GT.show Lam.ground) 1 q qh (REPR (fun q -> evalo (v varX) q))
-;;
-
-let _withFree =
-  runL 1 q qh (REPR (fun q -> evalo (app q (v varX)) (v varX)));
-  runL 1 qr qrh (REPR (fun q r -> evalo (app r q) (v varX)));
-  runL 2 qrs qrsh (REPR (fun q r s -> a_la_quine q r s))
-;;
+let () = print_endline "Hello, World!"
diff --git a/lib/lib.ml b/lib/lib.ml
index 2025d58..ac08465 100644
--- a/lib/lib.ml
+++ b/lib/lib.ml
@@ -1,17 +1,158 @@
 open OCanren
 
-module Lam = struct
-  [%%distrib
-  type nonrec ('varname, 'self) t =
-    | V of 'varname
-    | App of 'self * 'self
-    | Abs of 'varname * 'self
-  [@@deriving gt ~options:{ show; fmt; gmap }]
+(* TODO: lift to logic domain *)
+type tag = Ref | ConstRef | ShallowCopy | ConstShallowCopy | DeepCopy | NoneRef;;
+(* MoveShallowCopy ? *)
 
-  type ground = (GT.string, ground) t]
+type typ = UnitT | IntT | BoolT | RefT of typ | PairT of typ * typ;;
+type mode = InM | OutM | InOutM;;
+type arg = Arg of tag * mode * typ;;
 
-  let varX = !!"x"
-  let varY = !!"y"
-  let varF = !!"f"
-end
+type op = AddOp | SubOp | NotOp | LessOp | MoreOp | LessEqOp | MoreEqOp | EqOp | NotEqOp;;
 
+type expr = IntE of int
+          | BoolE of bool
+          | VarE of string
+          (* pair *)
+          | PairE of expr * expr
+          | FstE of expr
+          | SndE of expr
+          (* pointers *)
+          | DerefE of expr
+          | RefE of expr;;
+
+type stmt = DeclS of string * typ
+          | AssignS of string * expr (* TODO: rvalue exprs *)
+          | SeqS of stmt * stmt
+          | ExprS of expr
+          | CallS of string * string list (* TODO: exprs?? *)
+          | IfS of expr * stmt * stmt;;
+
+type func_def = {
+  f_args: arg list;
+  f_body: stmt;
+};;
+
+type prog = {
+  p_func: (string * func_def) list;
+  p_code: stmt;
+};;
+
+(* ------ *)
+
+type value = IntV of int
+           | BoolV of bool
+           | BoxV of string (* ref to box, lvalue *)
+           | RefV of value
+           | PairV of value * value
+           | UnitV;;
+
+module M = Map.Make (String);;
+
+type func_env = func_def M.t;;
+type 'a frame = {
+  f_vars: 'a M.t;
+};;
+type 'a state = {
+  s_func: func_env;
+  s_frames: 'a frame list;
+  (* s_value: 'a; *)
+};;
+
+let init_state prog = { s_func = prog.p_func |> List.to_seq |> M.of_seq;
+                        s_frames = [];
+                        (* s_value = UnitV; *)
+                      };;
+
+let find_func name state = M.find_opt name state.s_func
+
+let find_frame_var name frame = M.find_opt name frame.f_vars;;
+let rec find_frames_var name frames =
+  match frames with
+  | [] -> None
+  | fr :: frs -> (match find_frame_var name fr with
+                  | Some x -> Some x
+                  | None -> find_frames_var name frs);;
+let find_var name state = find_frames_var name state.s_frames;;
+
+let add_var name value state =
+  match state.s_frames with
+  | [] -> failwith "No frames found"
+  | fr :: frs -> { state with s_frames = {f_vars = M.add name value fr.f_vars} :: frs};;
+
+let update_frame_var name value frame =
+  if M.find_opt name frame.f_vars != None then Some {f_vars = M.add name value frame.f_vars} else None;;
+let rec update_frames_var name value frames =
+  match frames with
+  | [] -> None
+  | fr :: frs -> (match update_frame_var name value fr with
+                  | Some fr -> Some (fr :: frs)
+                  | None -> Option.map (fun frs -> fr :: frs) @@ update_frames_var name value frs);;
+let update_var name value state =
+  Option.map (fun frs -> {state with s_frames = frs}) @@
+             update_frames_var name value state.s_frames ;;
+
+let check_op_types expr state = ();;
+
+(* TODO *)
+(* let ( let* ) = Option.bind;; *)
+
+(* TODO *)
+(* TODO: handle refs in proper way *)
+(* NOTE: exprs are pure and do not change state *)
+let rec check_expr_types expr state =
+  match expr with
+  | IntE _ -> IntT
+  | BoolE b -> BoolT
+  | VarE name -> RefT (Option.get @@ find_var name state)
+  (* pair *)
+  | PairE (fst_e, snd_e) -> PairT (check_expr_types fst_e state, check_expr_types snd_e state)
+  | FstE e ->
+    (match check_expr_types e state with
+     | PairT (t, _) -> t
+     | _ -> failwith "Fst type error")
+  | SndE e ->
+    (match check_expr_types e state with
+     | PairT (_, t) -> t
+     | _ -> failwith "Snd type error")
+  (* pointers *)
+  | DerefE e ->
+    (match check_expr_types e state with
+     | RefT t -> t
+     | _ -> failwith "Deref type eror")
+  | RefE e -> RefT (check_expr_types e state);;
+
+let expect_eq fst_val snd_val msg =
+ if fst_val == snd_val then fst_val else failwith msg;;
+
+let expect_neq fst_val snd_val msg =
+ if fst_val != snd_val then fst_val else failwith msg;;
+
+(* TODO *)
+let rec check_stmt_types stmt (state : typ state) =
+  match stmt with
+  | DeclS (name, typ) -> add_var name typ state
+  | AssignS (name, val_e) ->
+    let val_t = check_expr_types val_e state in
+    (match find_var name state with
+     | Some t -> ignore @@ expect_eq t val_t "Can't assign value of the different type"
+     | None -> failwith "Varible to assign is not found");
+    state
+  | SeqS (fst_e, snd_e) ->
+    let state = check_stmt_types fst_e state in
+    check_stmt_types snd_e state
+  | ExprS e -> ignore @@ check_expr_types e state; state
+  | CallS (name, args) ->
+    let func = find_func name state in
+    (* (match *) 
+    (* ) *)
+    failwith "Unimplemened"
+  | IfS (cond_e, then_e, else_e) ->
+    ignore @@ expect_eq (check_expr_types cond_e state) BoolT "If condition is not bool";
+    failwith "Unimplemened"
+    ;;
+
+(* TODO *)
+let parse str = ();;
+(* TODO *)
+let eval stmt state = ();;