diff --git a/.github/workflows/todo-to-issue.yml b/.github/workflows/todo-to-issue.yml
new file mode 100644
index 0000000..fe89a87
--- /dev/null
+++ b/.github/workflows/todo-to-issue.yml
@@ -0,0 +1,27 @@
+name: "Run TODO to Issue"
+on: [ "push" ]
+jobs:
+  build:
+    runs-on: "ubuntu-latest"
+    steps:
+      - uses: "actions/checkout@v4"
+      - name: "TODO to Issue"
+        uses: "alstr/todo-to-issue-action@v5"
+        with:
+          INSERT_ISSUE_URLS: "true"
+          CLOSE_ISSUES: "true"
+          LANGUAGES: ".todo-to-issue-languages.json"
+      - name: Set Git user
+        run: |
+          git config --global user.name "github-actions[bot]"
+          git config --global user.email "github-actions[bot]@users.noreply.github.com"
+      - name: Commit and Push Changes
+        run: |
+          git add -A
+          if [[ `git status --porcelain` ]]; then
+            git commit -m "Automatically added GitHub issue links to TODOs"
+            git push origin main
+          else
+            echo "No changes to commit"
+          fi
+
diff --git a/.todo-to-issue-languages.json b/.todo-to-issue-languages.json
new file mode 100644
index 0000000..e787115
--- /dev/null
+++ b/.todo-to-issue-languages.json
@@ -0,0 +1,21 @@
+[
+  {
+    "language": "Lean 4",
+    "extensions": [
+      ".lean"
+    ],
+    "markers": [
+      {
+        "type": "line",
+        "pattern": "--"
+      },
+      {
+        "type": "block",
+        "pattern": {
+          "start": "/-",
+          "end": "-/"
+        }
+      }
+    ]
+  }
+]
\ No newline at end of file
diff --git a/Tibi/Compiler.lean b/Tibi/Compiler.lean
index c137d64..7a93743 100644
--- a/Tibi/Compiler.lean
+++ b/Tibi/Compiler.lean
@@ -8,16 +8,21 @@ open Wasm.Value
 
 inductive CompileError
 | OutOfBounds_Int64 (n : Int)
-
-def Expr.compile : Expr → Except CompileError (List Wasm.Instr)
-| .Const n =>
-    if h : (-Int64.size : Int) ≤ n ∧ n < Int64.size then
-      .ok [.i64__const <| Int64.mk ⟨n, h.right, h.left⟩]
-    else
-      .error <| .OutOfBounds_Int64 n
+| Unimplemented
 
 def CompileError.toString : CompileError → String
 | .OutOfBounds_Int64 n => s!"{n} is out of Int64 bounds, should be satisfied that -2{Nat.toSuperscriptString 63} ≤ n < 2{Nat.toSuperscriptString 63}"
+| .Unimplemented => "Unimplemented"
 
 instance : ToString CompileError where
   toString := CompileError.toString
+
+def Expr.compile : Expr ctx ty → Except CompileError (List Wasm.Instr)
+| .Const n =>
+    if h : (-Int64.size : Int) ≤ n ∧ n < Int64.size then
+      .ok [.i64.const <| Int64.mk ⟨n, h.right, h.left⟩]
+    else
+      .error <| .OutOfBounds_Int64 n
+| .Var x =>
+    .ok [.local.get x.idx]
+| _ => .error .Unimplemented
diff --git a/Tibi/Interpreter.lean b/Tibi/Interpreter.lean
index 57a1892..2a86948 100644
--- a/Tibi/Interpreter.lean
+++ b/Tibi/Interpreter.lean
@@ -5,11 +5,31 @@ import Tibi.Util
 
 namespace Tibi
 
-def Expr.eval : (e : Expr) → {{ r | Eval e r }}
-| .Const n =>
+def Expr.eval (env : Env ctx) : {ty : Ty} → (e : Expr ctx ty) → ty.dom → {{ r | Eval e r }}
+| _, .Const n, _ =>
     if h : (-Int64.size : Int) ≤ n ∧ n < Int64.size then
-      .found (.ok <| Int64.mk ⟨n, h.right, h.left⟩) <| Eval.Const h.right h.left
+      .found (.ok <| Int64.mk ⟨n, h.right, h.left⟩) <| .Const h.right h.left
     else
       Decidable.not_and_iff_or_not_not.mp h |>.by_cases
         (fun h => .found (.error <| .OutOfBounds_Int64 n) <| Eval.ConstErr_ge h)
         (fun h => .found (.error <| .OutOfBounds_Int64 n) <| Eval.ConstErr_lt h)
+| _, .Var x, _ =>
+    .found (.ok <| env.lookup x) <| .Var x env
+| .fn _ .int, .Lam e', x =>
+    match e'.eval (x :: env) () with
+    | .found (.ok v) h => .found (.ok <| fun _ => v) <| .Lam h
+    | _                => .unknown
+| .int, .App (dom := dom) e₁ e₂, _ =>
+    match dom with
+    | .int => -- dom.dom = Unit
+        match e₂.eval env () with
+        | .found (.ok v) h₂ =>
+            match e₁.eval env v with
+            | .found (.ok f) h₁ => .found (.ok (f v)) <| .App h₁ h₂
+            | _                 => .unknown
+        | _ =>
+            .unknown
+    | _ =>
+        .unknown
+| _, _, _ =>
+    .unknown
diff --git a/Tibi/Parser.lean b/Tibi/Parser.lean
index 69ca398..0616655 100644
--- a/Tibi/Parser.lean
+++ b/Tibi/Parser.lean
@@ -4,16 +4,20 @@ import Tibi.Syntax
 namespace Tibi
 
 inductive Parser.Error
-| ExpectedDigit (got : Char)
-| ExpectedNonZeroDigit (got : Char)
-| IOError (e : IO.Error)
+| ExpectedAsciiAlpha    (got : Char)
+| ExpectedAsciiAlphaNum (got : Char)
+| ExpectedDigit         (got : Char)
+| ExpectedNonZeroDigit  (got : Char)
+| IOError               (e : IO.Error)
 | Unconsumed (rest : String)
 
 def Parser.Error.toString : Parser.Error → String
-| ExpectedDigit got        => s!"Expected a digit, got '{got}'"
-| ExpectedNonZeroDigit got => s!"Expected a non-zero digit, got '{got}'"
-| IOError e                => s!"IO Error: {e}"
-| Unconsumed rest          => s!"\"{rest}\" was not consumed"
+| ExpectedAsciiAlpha got    => s!"Expected an ASCII alphabet character, got '{got}'"
+| ExpectedAsciiAlphaNum got => s!"Expected an ASCII alphanumeric character, got '{got}'"
+| ExpectedDigit got         => s!"Expected a digit, got '{got}'"
+| ExpectedNonZeroDigit got  => s!"Expected a non-zero digit, got '{got}'"
+| IOError e                 => s!"IO Error: {e}"
+| Unconsumed rest           => s!"\"{rest}\" was not consumed"
 
 instance : ToString Parser.Error where
   toString := Parser.Error.toString
@@ -62,41 +66,91 @@ private def intNumber : Parser Int :=
         | _ => sgn n
   )
 
-private def parser : Parser Expr :=
+private def enclose (pre : String) (p : Parser α) (post : String) : Parser α :=
+  keyword pre >> ws >> p >> ws >> keyword post
+
+private def asciiAlpha : Parser Char :=
+  ParserT.satisfy Char.isAlpha .ExpectedAsciiAlpha
+
+private def asciiAlphanum : Parser Char :=
+  ParserT.satisfy Char.isAlphanum .ExpectedAsciiAlphaNum
+
+private def ident : Parser String :=
   (
-    natNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
-      |>.map fun (n, _) => .Const n
-  )
-  <|> (
-    intNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
-      |>.map fun (n, _) => .Const n
+    asciiAlpha >> ParserT.repeatGreedily asciiAlphanum
+      |>.map fun (c, cs) => String.mk (c :: cs)
   )
 
-instance : Inhabited (Parser Expr) where
-  default := parser
-
-private partial def parse' : ReaderT (IO String) Parser Expr := do
+private def var : Parser String :=
+  keyword "$" >> ident
+
+instance : Inhabited (Parser (Expr ctx .int)) where
+  default := intNumber.map Expr.Const
+
+mutual
+
+  partial def cls (x : Locals i ctx dom) : Parser (Expr ctx dom) :=
+    (
+      var >> ws
+        |>.map fun _ => .Var x
+    )
+
+  partial def fn : Parser (Expr ctx (.fn .int .int)) :=
+    (
+      var >> ws >> keyword "." >> ws >> cls (Locals.stop) >> ws
+        |>.map fun (_, e) => Expr.Lam e
+    )
+
+  partial def expr : Parser (Expr .nil .int) :=
+    (
+      natNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
+        |>.map fun n => .Const n
+    )
+    <|> (
+      intNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
+        |>.map fun n => .Const n
+    )
+    <|> (
+      enclose "(" fn ")" >> ws >> expr >> ws
+        |>.map fun (f, e) => .App f e
+    )
+    -- <|> (
+    --   keyword "it" >> ws
+    --     |>.map fun _ => .Var .stop
+    -- )
+end
+
+private partial def parse' : ReaderT (IO String) Parser (Expr .nil .int) := do
   fun getLine cs =>
-    match parser cs with
-    | .error .UnexpectedEndOfInput => do
+    match expr cs with
+    | .ok (e, []) =>
         match getLine () with
-        | .ok s _    => parse' getLine <| cs.append s.data
-        | .error e _ => Except.error <| Parser.Error.IOError e
+        | .ok s _    =>
+            if s.isEmpty then
+              .ok (e, [])
+            else
+              .error $ .ExpectedEndOfInput s.trimRight.data
+        | .error e _ =>
+            .error $ Parser.Error.IOError e
+    | .ok (_, cs) =>
+        .error $ .ExpectedEndOfInput cs
+    | .error .UnexpectedEndOfInput => -- continue to parse furthermore
+        match getLine () with
+        | .ok s _    =>
+            if s.isEmpty then
+              .error $ .UnexpectedEndOfInput
+            else
+              parse' getLine $ cs.append s.data
+        | .error e _ => .error $ Parser.Error.IOError e
     | v => v
 
--- #eval parse' (pure "0120") "123".data
--- #eval parse' (pure "-1") "".data
--- #eval parse' (pure "9223372036854775808") "".data
--- #eval parse' (pure "9223372036854775808") "".data
--- #eval parse' (pure "0120") "123".data
-
-def parse (stream : IO.FS.Stream) :=
+def parse (stream : IO.FS.Stream): IO (Option (ParserT.Result Char Parser.Error Id (Expr .nil .int))) :=
   stream.getLine >>= pure ∘ fun s =>
     match s.data with
     | [] => none
     | cs => some <| parse' stream.getLine cs
 
-def parseLine (line : String) :=
+def parseLine (line : String) : Option (ParserT.Result Char Parser.Error Id (Expr .nil .int)) :=
   match line.data with
   | [] => none
   | cs => some <| parse' (pure "") cs
diff --git a/Tibi/ParserT/Combinator.lean b/Tibi/ParserT/Combinator.lean
index 1ec96dd..5ea43ee 100644
--- a/Tibi/ParserT/Combinator.lean
+++ b/Tibi/ParserT/Combinator.lean
@@ -13,6 +13,12 @@ def hAndThen (p : ParserT σ ε m α) (q : Unit → ParserT σ ε m β) : Parser
 instance : HAndThen (ParserT σ ε m α) (ParserT σ ε m β) (ParserT σ ε m (α × β)) where
   hAndThen := hAndThen
 
+instance : HAndThen (ParserT σ ε m Unit) (ParserT σ ε m β) (ParserT σ ε m β) where
+  hAndThen p q := p.hAndThen q >>= pure ∘ Prod.snd
+
+instance : HAndThen (ParserT σ ε m α) (ParserT σ ε m Unit) (ParserT σ ε m α) where
+  hAndThen p q := p.hAndThen q >>= pure ∘ Prod.fst
+
 -- def hOrElse (p : ParserT σ ε m α) (q : Unit → ParserT σ ε m β) : ParserT σ ε m (α ⊕ β) :=
 --   fun cs =>
 --     ExceptT.tryCatch
diff --git a/Tibi/Props/Compiler.lean b/Tibi/Props/Compiler.lean
index ac6793f..707f6b3 100644
--- a/Tibi/Props/Compiler.lean
+++ b/Tibi/Props/Compiler.lean
@@ -4,15 +4,36 @@ import Tibi.Wasm.Semantics
 
 namespace Tibi
 
-theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok -- Expr.compile_ok_of_has_type_of_eval
-: {e : Expr} → HasType e _ty → Eval e (.ok v) → {_ : e.compile = .ok instrs}
+-- TODO prove Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok
+/-
+type mismatch
+  Wasm.Reduction.local__get ↑x.idx
+has type
+  Wasm.Reduction
+    { stack := ?m.4159, store := ?m.4160, framestate := ?m.4161, instrs := Wasm.Instr.local.get ↑x.idx :: ?m.4162 }
+    { stack := Wasm.StackValue.Value (?m.4161.locals.get! ↑x.idx) :: ?m.4159, store := ?m.4160, framestate := ?m.4161,
+      instrs := ?m.4162 } : Prop
+but is expected to have type
+  Wasm.Reduction
+    { stack := stack, store := store, framestate := framestate, instrs := [Wasm.Instr.local.get ↑x.idx] ++ K }
+    { stack := Wasm.StackValue.Value (Wasm.Value.Num (Wasm.Num.Int64 (Env.lookup x env))) :: stack, store := store,
+      framestate := framestate, instrs := K } : Prop
+
+theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok
+: {e : Expr ctx ty} → HasType env e _ty → Eval env e (.ok v) → {_ : e.compile = .ok instrs}
 → Wasm.Reduction
     { instrs := instrs ++ K, stack,                                      store, framestate }
     { instrs := K,           stack := .Value (.Num (.Int64 v)) :: stack, store, framestate }
 | .Const n, .Int64 hLt hGe, .Const _ _, hc => by
-    have : (Expr.Const n).compile = .ok [.i64__const (Int64.mk ⟨n, hLt, hGe⟩)] := by
+    have : (Expr.Const n : Expr ctx ty).compile = .ok [.i64.const (Int64.mk ⟨n, hLt, hGe⟩)] := by
       -- dsimp [Expr.compile]
       apply dite_cond_eq_true <| eq_true <| And.intro hGe hLt
-    have : instrs = [.i64__const ⟨n, hLt, hGe⟩ ] := Except.ok.inj <| Eq.trans hc.symm this
+    have : instrs = [.i64.const ⟨n, hLt, hGe⟩] := Except.ok.inj <| Eq.trans hc.symm this
+    rw [this]
+    exact .i64.const
+| .Var x, .Var, .Var _, hc => by
+    have : (Expr.Var x : Expr ctx ty).compile = .ok [.local.get x.idx] := rfl
+    have : instrs = [.local.get x.idx] := Except.ok.inj <| Eq.trans hc.symm this
     rw [this]
-    exact .i64__const
+    exact .local.get x.idx
+-/
diff --git a/Tibi/Props/Typing.lean b/Tibi/Props/Typing.lean
index ad1ca9a..d8e3b97 100644
--- a/Tibi/Props/Typing.lean
+++ b/Tibi/Props/Typing.lean
@@ -3,27 +3,62 @@ import Tibi.Typing
 
 namespace Tibi
 
-theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
-  cases h₁ <;> cases h₂ <;> rfl
+theorem HasType.det : HasType e t₁ → HasType e t₂ → t₁ = t₂
+| .Int64 ..,  .Int64 ..    => rfl
+| .Var,       .Var         => rfl
+| .Lam h,     .Lam h'      => by rw [h.det h']
+| .App h₁ h₂, .App h₁' h₂' => h₂.det h₂' ▸ h₁.det h₁' |> Typ.Fn.inj |>.right
 
-theorem Expr.typeCheck_correct {e : Expr}
-: (ht : HasType e ty) → e.typeCheck = .found ty ht
-| .Int64 (n := n) hLt hGe =>
-    have := eq_true <| And.intro (ge_iff_le.mp hGe) hLt
-    dite_cond_eq_true this
+/--
+Reference: [A Certified Type Checker \- Lean Documentation Overview](https://lean-lang.org/lean4/doc/examples/tc.lean.html)
+-/
+theorem Expr.typeCheck_correct {e : Expr ctx ty}
+  (ht : HasType e t)
+  (h : e.typeCheck ≠ .unknown)
+: e.typeCheck = .found t ht
+:= by
+  revert h
+  match e.typeCheck with
+  | .found ty' h₁' => intro ; have := ht.det h₁' ; subst this ; rfl
+  | .unknown       => intros; contradiction
+/-
+Try this: (match e.typeCheck with
+  | Maybe.found ty' h₁' => fun h =>
+    let_fun this := HasType.det ht h₁';
+    Eq.ndrec (motive := fun ty' =>
+      ∀ (h₁' : HasType e ty'), Maybe.found ty' h₁' ≠ Maybe.unknown → Maybe.found ty' h₁' = Maybe.found t ht)
+      (fun h₁' h => Eq.refl (Maybe.found t h₁')) this h₁' h
+  | Maybe.unknown => fun h => absurd (Eq.refl Maybe.unknown) h)
+  h
+-/
 
-theorem Expr.typeCheck_complete {e : Expr}
-: e.typeCheck = .unknown → ¬ HasType e ty
+-- TODO prove Expr.typeCheck_complete
+/-
+theorem Expr.typeCheck_complete {e : Expr ctx ty}
+: e.typeCheck = .unknown → ¬HasType e t
 := by
-  dsimp [Expr.typeCheck]
-  intro h (ht : HasType e ty)
-  match ht with
-  | .Int64 hLt hGe =>
-      have := eq_true <| And.intro (ge_iff_le.mp hGe) hLt
-      have := h ▸ dite_cond_eq_true this
-      exact Maybe.noConfusion this
+  induction e with simp [Expr.typeCheck]
+  | Const n =>
+      intro h ht
+      match ht with
+      | .Int64 hLt hGe =>
+          have := h hGe hLt
+          contradiction
+  | Lam e ih =>
+      match h : e.typeCheck with
+      | .found t' ht' => intro ; contradiction
+      | .unknown =>
+          have : ¬HasType e t := ih h
+          intro _ ht'
+          match ht' with
+          | .Lam h' =>
+              sorry
+  | App e₁ e₂ ih₁ ih₂ => sorry
+-/
 
-instance (e : Expr) (t : Typ) : Decidable (HasType e t) :=
+-- TODO prove : Decidable (HasType e t)
+/-
+instance (e : Expr ctx ty) (t : Typ) : Decidable (HasType e t) :=
   match h : e.typeCheck with
   | .found t' ht' =>
       if heq : t = t' then
@@ -31,9 +66,14 @@ instance (e : Expr) (t : Typ) : Decidable (HasType e t) :=
       else
         isFalse fun ht => heq (HasType.det ht ht')
   | .unknown => isFalse (Expr.typeCheck_complete h)
+-/
 
-theorem type_safe {e : Expr}
+-- TODO prove type_safe
+/-
+theorem type_safe {e : Expr ctx ty}
 : HasType e t → Eval e r → ∃ v, r = .ok v
 | .Int64 hLt hGe, .Const ..      => ⟨Int64.mk ⟨_, hLt, hGe⟩, rfl⟩
 | .Int64 hLt _,   .ConstErr_lt h => absurd hLt h
 | .Int64 _   hGe, .ConstErr_ge h => absurd hGe h
+| .Var,           .Var x => ⟨env.lookup x, rfl⟩
+-/
diff --git a/Tibi/Semantics.lean b/Tibi/Semantics.lean
index f668ba3..0b88a11 100644
--- a/Tibi/Semantics.lean
+++ b/Tibi/Semantics.lean
@@ -1,18 +1,2 @@
-import Tibi.FinInt
-import Tibi.Syntax
-
-namespace Tibi
-
-inductive EvalError
-| OutOfBounds_Int64 (n : Int)
-
-inductive Eval : Expr → Except EvalError Int64 → Prop
-| Const       {n : Int} (hLt : n < Int64.size) (hGe : n >= -Int64.size) : Eval (.Const n) (.ok <| Int64.mk ⟨n, hLt, hGe⟩)
-| ConstErr_lt {n : Int} (h : ¬ n < Int64.size)   : Eval (.Const n) (.error <| .OutOfBounds_Int64 n)
-| ConstErr_ge {n : Int} (h : ¬ n >= -Int64.size) : Eval (.Const n) (.error <| .OutOfBounds_Int64 n)
-
-def EvalError.toString : EvalError → String
-| .OutOfBounds_Int64 n => s!"{n} is out of Int64 bounds, should be satisfied that -2{Nat.toSuperscriptString 63} ≤ n < 2{Nat.toSuperscriptString 63}"
-
-instance : ToString EvalError where
-  toString := EvalError.toString
+import Tibi.Semantics.Env
+import Tibi.Semantics.Eval
diff --git a/Tibi/Semantics/Env.lean b/Tibi/Semantics/Env.lean
new file mode 100644
index 0000000..07dfeff
--- /dev/null
+++ b/Tibi/Semantics/Env.lean
@@ -0,0 +1,14 @@
+import Tibi.Syntax
+import Tibi.Util
+
+namespace Tibi
+
+inductive Env : Vec Ty n → Type where
+| nil  : Env Vec.nil
+| cons : Ty.interp a → Env ctx → Env (a :: ctx)
+
+infix:67 " :: " => Env.cons
+
+def Env.lookup : Locals i ctx ty → Env ctx → ty.interp
+| .stop,  x :: _  => x
+| .pop k, _ :: xs => xs.lookup k
diff --git a/Tibi/Semantics/Eval.lean b/Tibi/Semantics/Eval.lean
new file mode 100644
index 0000000..8d79037
--- /dev/null
+++ b/Tibi/Semantics/Eval.lean
@@ -0,0 +1,30 @@
+import Tibi.FinInt
+import Tibi.Semantics.Env
+import Tibi.Syntax
+
+namespace Tibi
+
+inductive EvalError
+| OutOfBounds_Int64 (n : Int)
+
+def EvalError.toString : EvalError → String
+| .OutOfBounds_Int64 n => s!"{n} is out of Int64 bounds, should be satisfied that -2{Nat.toSuperscriptString 63} ≤ n < 2{Nat.toSuperscriptString 63}"
+
+instance : ToString EvalError where
+  toString := EvalError.toString
+
+inductive Eval : (Expr ctx ty) → Except EvalError ty.interp → Prop
+| Const {n : Int} (hLt : n < Int64.size) (hGe : n >= -Int64.size)
+  : Eval (.Const n) (.ok <| Int64.mk ⟨n, hLt, hGe⟩)
+| ConstErr_lt {n : Int} (h : ¬ n < Int64.size)
+  : Eval (.Const n) (.error <| .OutOfBounds_Int64 n)
+| ConstErr_ge {n : Int} (h : ¬ n >= -Int64.size)
+  : Eval (.Const n) (.error <| .OutOfBounds_Int64 n)
+-- | Var' (env : Env (α :: .nil)) (a : α.interp) -- {x : Locals 0 (a :: ctx) a}
+--   : Eval (.Var Locals.stop) (.ok <| a)
+| Var (x : Locals k ctx ty) (env : Env ctx)
+  : Eval (.Var x) (.ok <| env.lookup x)
+| Lam (d : Eval e (.ok v))
+  : Eval (.Lam e) (.ok <| fun _ => v)
+| App (d₁ : Eval e₁ (.ok f)) (d₂ : Eval e₂ (.ok x))
+  : Eval (.App e₁ e₂) (.ok <| f x)
diff --git a/Tibi/Syntax/Expr.lean b/Tibi/Syntax/Expr.lean
index f04d64e..795ebbc 100644
--- a/Tibi/Syntax/Expr.lean
+++ b/Tibi/Syntax/Expr.lean
@@ -1,10 +1,51 @@
 import Tibi.FinInt
+import Tibi.Util
 
 namespace Tibi
 
-inductive Expr
-| Const : Int → Expr
+inductive Ty where
+| int
+| fn (a b : Ty)
 
-instance : ToString Expr where
-  toString
-  | .Const n => s!"<Const {n}>"
+@[reducible]
+def Ty.interp : Ty → Type
+| int     => Int64
+| fn a b  => a.interp → b.interp
+
+@[reducible]
+def Ty.dom : Ty → Type
+| int     => Unit
+| fn a _  => a.interp
+
+def Ty.toString : Ty → String
+| int     => "Int"
+| fn a b  => s!"{a.toString} -> {b.toString}"
+
+instance : ToString Ty where
+  toString := Ty.toString
+
+inductive Locals : Fin n → Tibi.Vec Ty n → Ty → Type where
+| stop : Locals 0 (ty :: ctx) ty
+| pop  : Locals k ctx ty → Locals k.succ (u :: ctx) ty
+
+def Locals.idx : Locals n ctx ty → Fin n.succ
+| stop  => Fin.mk 0 (Fin.succ_pos _)
+| pop k => k.idx.succ
+
+instance : ToString (Locals n ctx ty) where
+  toString x := s!"${x.idx}"
+
+inductive Expr : Vec Ty n → Ty → Type where
+| Const : Int → Expr ctx .int
+| Var   : Locals i ctx ty → Expr ctx ty
+| Lam   : Expr (dom :: ctx) ran → Expr ctx (.fn dom ran)
+| App   : Expr ctx (.fn dom ran) → Expr ctx dom → Expr ctx ran
+
+def Expr.toString : Expr ctx ty → String
+| Const n => s!"<Const {n}>"
+| Var x   => s!"<Var {x} @{ty}>"
+| Lam e   => s!"<Lam {e.toString}>"
+| App e₁ e₂ => s!"<App {e₁.toString} {e₂.toString}>"
+
+instance : ToString (Expr ctx ty) where
+  toString := Expr.toString
diff --git a/Tibi/Top.lean b/Tibi/Top.lean
index abab511..3c613b3 100644
--- a/Tibi/Top.lean
+++ b/Tibi/Top.lean
@@ -6,7 +6,7 @@ import Tibi.Typing
 namespace Tibi
 
 partial def repl (stream : IO.FS.Stream) (n : Nat := 0) : IO UInt32 := do
-  IO.print s!"{n}:> "
+  if ← stream.isTty then IO.print s!"{n}:> "
   let line ← stream.getLine
   if not line.isEmpty then
     if let some r := parseLine line then
@@ -14,7 +14,7 @@ partial def repl (stream : IO.FS.Stream) (n : Nat := 0) : IO UInt32 := do
       | .ok (expr, []) =>
           match expr.typeCheck with
           | .found t _ =>
-              match expr.eval with
+              match expr.eval .nil () with
               | .found (.ok v) _    => IO.println s!"- : {t} = {v}"
               | .found (.error _) _ => panic! "TODO: prove that this branch cannot be reached (type-safe)"
               | .unknown            => panic! "TODO: prove that this branch cannot be reached (type-safe)"
@@ -37,7 +37,7 @@ def run (inStream : IO.FS.Stream) : IO ByteArray :=
       | .some <| .error e       => .throw e.toString
   )
   >>= (
-    fun (e : Option Expr) =>
+    fun (e : Option (Expr _ _)) =>
       match e with
       | .none   => pure Wasm.empty
       | .some e =>
diff --git a/Tibi/Typing.lean b/Tibi/Typing.lean
index a367b7e..3812676 100644
--- a/Tibi/Typing.lean
+++ b/Tibi/Typing.lean
@@ -1,25 +1,52 @@
 import Tibi.FinInt
+import Tibi.Semantics
 import Tibi.Syntax
 import Tibi.Util
 
 namespace Tibi
 
 inductive Typ
+| Var (idx : Nat)
 | Int64
+| Fn (a : Typ) (b : Typ)
 deriving DecidableEq
 
 def Typ.toString : Typ → String
-| Int64 => "Int"
+| Var idx => s!"α{idx}"
+| Int64   => "Int"
+| Fn a b  => s!"{a.toString} -> {b.toString}"
 
 instance : ToString Typ where
   toString := Typ.toString
 
-inductive HasType : Expr → Typ → Prop
+def Ty.toTyp : Ty → Typ
+| int     => .Int64
+| fn a b  => .Fn a.toTyp b.toTyp
+
+inductive HasType : Expr ctx ty → Typ → Prop
 | Int64 {n : Int} (hLt : n < Int64.size) (hGe : n ≥ -Int64.size) : HasType (.Const n) .Int64
+| Var {x : Locals i ctx ty} : HasType (.Var x) ty.toTyp
+| Lam (h : HasType e t) : HasType (.Lam e) (.Fn .Int64/-(.Var 0)-/ t)
+| App (hf : HasType f (.Fn dom ran)) (hv : HasType v dom) : HasType (.App f v) ran
 
-def Expr.typeCheck : (e : Expr) → {{ t | HasType e t }}
+def Expr.typeCheck : (e : Expr ctx ty) → {{ t | HasType e t }}
 | .Const n =>
     if h : -Int64.size ≤ n ∧ n < Int64.size then
       .found .Int64 <| .Int64 h.right h.left
     else
       .unknown
+| .Var _ =>
+    .found _ .Var
+| .Lam e =>
+    match e.typeCheck with
+    | .found t h => .found (.Fn .Int64/-(.Var 0)-/ t) <| .Lam h
+    | .unknown   => .unknown
+| .App f v =>
+    match f.typeCheck, v.typeCheck with
+    | .found (.Fn a b) hf, .found a' hv =>
+        if h : a = a' then
+          .found b <| .App hf (h ▸ hv)
+        else
+          .unknown
+    | _, _ => .unknown
+-- | _ => .unknown
diff --git a/Tibi/Util.lean b/Tibi/Util.lean
index 0c46d05..f088589 100644
--- a/Tibi/Util.lean
+++ b/Tibi/Util.lean
@@ -9,3 +9,9 @@ inductive Maybe (p : α → Prop)
 | found (a : α) : p a → Maybe p
 
 notation "{{ " x " | " p " }}" => Maybe (fun x => p)
+
+inductive Vec (α : Type u) : Nat → Type u
+| nil : Vec α 0
+| cons : α → Vec α n → Vec α n.succ
+
+infixr:67 " :: " => Vec.cons
diff --git a/Tibi/Wasm/Instruction.lean b/Tibi/Wasm/Instruction.lean
index b463e9f..10e3c4d 100644
--- a/Tibi/Wasm/Instruction.lean
+++ b/Tibi/Wasm/Instruction.lean
@@ -10,10 +10,15 @@ open Wasm.Value
 
 inductive Instr
 -- Numeric Instructions
-| i32__const (i : Int32)
-| i64__const (i : Int64)
+| i32.const (i : Int32)
+| i64.const (i : Int64)
+-- Variable Instructions
+| local.get (i : Nat)
+
+def Instr.encode : Instr → List UInt8
+| i32.const i => 0x41 :: i.encode
+| i64.const i => 0x42 :: i.encode
+| local.get i => 0x42 :: (Encoder.encode 128) ++ 0x21 :: Encoder.encode i ++ 0x20 :: Encoder.encode i
 
 instance : Encoder Instr where
-  encode
-    | .i32__const i => 0x41 :: i.encode
-    | .i64__const i => 0x42 :: i.encode
+  encode := Instr.encode
diff --git a/Tibi/Wasm/Module/Basic.lean b/Tibi/Wasm/Module/Basic.lean
index 43fa22c..64bc885 100644
--- a/Tibi/Wasm/Module/Basic.lean
+++ b/Tibi/Wasm/Module/Basic.lean
@@ -36,7 +36,7 @@ open Wasm (Code Export FuncType Section)
 def Wasm.magic : List UInt8 := [0x00, 0x61, 0x73, 0x6D]
 def Wasm.version : List UInt8 := [0x01, 0x00, 0x00, 0x00]
 
--- TODO https://webassembly.github.io/spec/core/syntax/modules.html#syntax-module
+-- XXX https://webassembly.github.io/spec/core/syntax/modules.html#syntax-module
 structure Wasm where
   types : List FuncType
   funcs : List Nat
diff --git a/Tibi/Wasm/Semantics/Basic.lean b/Tibi/Wasm/Semantics/Basic.lean
index e83ffc5..78e2ac5 100644
--- a/Tibi/Wasm/Semantics/Basic.lean
+++ b/Tibi/Wasm/Semantics/Basic.lean
@@ -18,6 +18,9 @@ inductive Num
 inductive Value
 | Num (n : Num)
 
+instance : Inhabited Value where
+  default := .Num (.Int64 (Tibi.Int64.ofFin 0))
+
 /- ### Activation Frames -/
 
 structure FrameState where
diff --git a/Tibi/Wasm/Semantics/Reduction.lean b/Tibi/Wasm/Semantics/Reduction.lean
index 6d102e0..c5932a0 100644
--- a/Tibi/Wasm/Semantics/Reduction.lean
+++ b/Tibi/Wasm/Semantics/Reduction.lean
@@ -9,9 +9,12 @@ open Wasm.Value
 /- # Wasm Reduction -/
 
 inductive Reduction : Configuration → Configuration → Prop
-| i32__const {i : Int32} : Reduction
-    { instrs := .i32__const i :: K, stack := s,                             store, framestate }
+| i32.const {i : Int32} : Reduction
+    { instrs := .i32.const i :: K, stack := s,                             store, framestate }
     { instrs := K,                  stack := .Value (.Num (.Int32 i)) :: s, store, framestate }
-| i64__const {i : Int64} : Reduction
-    { instrs := .i64__const i :: K, stack := s,                             store, framestate }
+| i64.const {i : Int64} : Reduction
+    { instrs := .i64.const i :: K, stack := s,                             store, framestate }
     { instrs := K,                  stack := .Value (.Num (.Int64 i)) :: s, store, framestate }
+| local.get (n : Nat) : Reduction
+    { instrs := .local.get n :: K, stack := s,                                      store, framestate }
+    { instrs := K,                  stack := .Value (framestate.locals.get! n) :: s, store, framestate }