diff --git a/Main.lean b/Main.lean
index 29206ada..1cb501b7 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,10 +1,4 @@
-import Yatima.Cli.ContAddrCmd
-import Yatima.Cli.TypecheckCmd
-import Yatima.Cli.CodeGenCmd
-import Yatima.Cli.ProveCmd
-import Yatima.Cli.VerifyCmd
-import Yatima.Cli.IpfsCmd
-import Yatima.Cli.PrintPrimsCmd
+import Yatima
 
 opaque VERSION : String :=
   s!"{Lean.versionString}|0.0.1"
diff --git a/Yatima.lean b/Yatima.lean
index 7538cf30..f50e83c8 100644
--- a/Yatima.lean
+++ b/Yatima.lean
@@ -31,6 +31,8 @@ import Yatima.CodeGen.Preloads
 import Yatima.CodeGen.PrettyPrint
 import Yatima.CodeGen.Simp
 import Yatima.CodeGen.Test
+import Yatima.Compiler.Yul
+import Yatima.Compiler.Grin
 import Yatima.ContAddr.ContAddr
 import Yatima.ContAddr.ContAddrError
 import Yatima.ContAddr.ContAddrM
diff --git a/Yatima/Compiler/Compiler.lean b/Yatima/Compiler/Compiler.lean
new file mode 100644
index 00000000..5c887145
--- /dev/null
+++ b/Yatima/Compiler/Compiler.lean
@@ -0,0 +1,84 @@
+import Yatima.Compiler.GrinM
+import Yatima.Compiler.Debug
+import Lean.Expr
+open Lean.Compiler.LCNF
+
+def Lean.FVarId.toVar (id : Lean.FVarId) : Yatima.Grin.Var := .mk id.name
+
+namespace Yatima.Grin
+
+def mkFreshVar : GrinM Var := do
+  pure ⟨← Lean.mkFreshId⟩
+
+def paramsToVars (params : Array Param) : List Var :=
+  params.toList.map (fun param => param.fvarId.toVar)
+
+def fetch? (id : Lean.FVarId) : GrinM SExpr := do
+  match ← varKind id with
+  | .pointer => pure $ .fetch id.toVar .none
+  | .basic => pure $ svar id.toVar
+
+def applyArgs (fnc : Var) : (args : List Arg) → GrinM Expr
+| [] => pure $ .ret $ svar fnc
+| .erased :: args => applyArgs fnc args
+| .type _ :: args => applyArgs fnc args
+| .fvar id :: args => do
+  let apply := .apply fnc (.var id.toVar)
+  let newVar ← mkFreshVar
+  let rest ← applyArgs newVar args
+  pure $ .seq apply (.svar newVar) rest
+
+mutual
+partial def PScheme : Alt → GrinM (CPat × Expr)
+| .default code => do
+  let expr ← RScheme code
+  pure (.default, expr)
+| .alt ctor params code  => do
+  let args := paramsToVars params
+  let tag := .C ⟨ ctor ⟩
+  let expr ← RScheme code
+  pure (.ctag tag args, expr)
+
+partial def RScheme : Code → GrinM Expr
+| .let decl k => match decl.value with
+  | .erased => RScheme k
+  | .value val => do
+    pure $ .ret $ slit val
+  | .proj _ idx struct => do
+    let structPtr := struct.toVar
+    let proj := .fetch structPtr (some idx)
+    pure $ .ret proj
+  | .const _name _ _args => throw "TODO"
+  | .fvar fnc args => do
+    let fncVal ← fetch? fnc
+    let newVar ← mkFreshVar
+    pure $ .seq fncVal (.svar newVar) (← applyArgs newVar args.toList)
+| .cases case => do
+  let some patExprs := NEList.nonEmpty (← case.alts.toList.mapM PScheme)
+    | throw "Empty pattern"
+  -- Since every variable is initially strict, we don't need to eval before
+  let caseVal ← fetch? case.discr
+  let newVar ← mkFreshVar
+  let caseExpr := .case (.sval $ .var newVar) patExprs
+  pure $ .seq caseVal (.svar newVar) caseExpr
+  -- pure expr
+| .return fvarId => do
+  -- In the lazy case, a return is a call to eval, but since we chose strict semantics this
+  -- will either be a `fetch` or `unit` instruction depending on whether the variable is a
+  -- pointer or basic value
+  pure $ .ret $ ← fetch? fvarId
+| .fun _decl _k => throw "Should not find function definition here (?)"
+-- We need to figure out a way to implement join points
+| .jp _decl _k => throw "TODO"
+| .jmp _fvarId _args => throw "TODO"
+| .unreach _type => throw "Unreach found"
+end
+
+def compileDeclaration (decl : Decl) : GrinM Binding := do
+  let defn := ⟨decl.name⟩
+  let args := paramsToVars decl.params
+  let body ← RScheme decl.value
+  let binding := { defn, args, body }
+  pure binding
+
+end Yatima.Grin
diff --git a/Yatima/Compiler/Debug.lean b/Yatima/Compiler/Debug.lean
new file mode 100644
index 00000000..a27ca694
--- /dev/null
+++ b/Yatima/Compiler/Debug.lean
@@ -0,0 +1,59 @@
+import Lean.Compiler.LCNF
+open Lean.Compiler.LCNF
+
+namespace Lean.Compiler.LCNF
+
+instance : ToString FVarId where
+  toString x := toString x.name
+
+instance : ToString Param where
+  toString x := s!"{x.fvarId}"
+
+instance [ToString K] : ToString (AltCore K) where
+  toString
+    | .alt ctor params k => s!"{ctor} {params} => {k}"
+    | .default k => s!"_ => {k}"
+
+instance : ToString LitValue where
+  toString
+  | .natVal x => s!"{x}"
+  | .strVal x => s!"\"{x}\""
+
+instance : ToString Arg where
+  toString
+  | .erased => "ε"
+  | .type .. => "τ"
+  | .fvar id => s!"{id}"
+
+instance : ToString LetValue where
+  toString
+    | .value lit => s!"{lit}"
+    | .erased .. => "ε"
+    | .proj _ idx struct => s!"(π {idx} {struct})"
+    | .const cnst _ args => s!"(const {cnst} {args})"
+    | .fvar id args => s!"(fvar {id} {args})"
+
+instance : ToString LetDecl where
+  toString decl := s!"{decl.fvarId} := {decl.value}"
+
+instance [ToString K] : ToString (FunDeclCore K) where
+  toString decl := s!"{decl.fvarId} {decl.params} := {decl.value}"
+
+instance [ToString K] : ToString (CasesCore K) where
+  toString cases := s!"{cases.discr} {cases.alts}"
+
+partial def Code.toString (code : Code) : String :=
+  let _ : ToString Code := ⟨toString⟩
+  match code with
+  | .let decl k => s!"(let {decl} in {k})"
+  | .fun decl k => s!"(fun {decl} in {k})"
+  | .jp decl k => s!"(jp {decl} in {k})"
+  | .jmp id args => s!"(jmp {id} {args})"
+  | .cases case => s!"(match {case})"
+  | .return id => s!"(return {id.name})"
+  | .unreach _ => "unreach"
+
+instance : ToString Code where
+  toString code := code.toString
+
+end Lean.Compiler.LCNF
diff --git a/Yatima/Compiler/Grin.lean b/Yatima/Compiler/Grin.lean
new file mode 100644
index 00000000..414a704f
--- /dev/null
+++ b/Yatima/Compiler/Grin.lean
@@ -0,0 +1,85 @@
+import Lean.Expr
+import Lean.Compiler.LCNF
+import YatimaStdLib.NonEmpty
+
+open Lean.Compiler.LCNF
+
+-- Based on https://nbviewer.org/github/grin-compiler/grin/blob/master/papers/boquist.pdf
+namespace Yatima.Grin
+
+/-- Var represents a variable binding, such as in a function definition in a pattern -/
+structure Var where
+  data : Lean.Name
+/-- Id represents a known definition, such as a function or constructor -/
+structure Id where
+  data : Lean.Name
+/-- VarKind tells us whether a variable is a pointer or a basic value -/
+inductive VarKind
+| pointer
+| basic
+
+inductive Tag where
+-- Suspended full applications
+| F : Id → Tag
+-- Partial applications
+| P : Id → Nat → Tag
+-- Saturated constructors
+| C : Id → Tag
+
+abbrev Literal := LitValue
+
+inductive SVal where
+  | lit : Literal → SVal
+  | var : Var → SVal
+
+inductive Val where
+  | ctag  : Tag → List SVal → Val
+  | stag  : Tag → Val
+  | empty : Val
+  | sval  : SVal → Val
+
+inductive CPat where
+  -- Complete tag pattern
+  | ctag : Tag → List Var → CPat
+  -- Single tag pattern
+  | stag : Tag → CPat
+  -- Default case
+  | default : CPat
+  | lit  : Literal → CPat
+
+inductive LPat where
+  | ctag  : Tag → List SVal → LPat
+  | cvar  : Var → List SVal → LPat
+  | stag  : Tag → LPat
+  | svar  : Var → LPat
+
+inductive SExpr where
+  | unit   : Val → SExpr
+  | store  : Val → SExpr
+  | fetch  : Var → Option Nat → SExpr
+  | update : Var → Val → SExpr
+  -- Known function call
+  | call   : Id → NEList SVal → SExpr
+  -- Evaluation of unknown expression
+  | eval   : Var → SExpr
+  -- Application of unknown function to a list of arguments
+  | apply  : Var → SVal → SExpr
+
+inductive Expr where
+  | ret  : SExpr → Expr
+  | seq  : SExpr → LPat → Expr → Expr
+  | join : Expr → LPat → Expr → Expr
+  | case : Val → NEList (CPat × Expr) → Expr
+
+structure Binding where
+  defn : Id
+  args : List Var
+  body : Expr
+
+abbrev Prog := NEList Binding
+
+-- Helper functions
+def svar (var : Var) : SExpr := .unit $ .sval $ .var var
+def slit (lit : Literal) : SExpr := .unit $ .sval $ .lit lit
+
+end Yatima.Grin
diff --git a/Yatima/Compiler/GrinM.lean b/Yatima/Compiler/GrinM.lean
new file mode 100644
index 00000000..05384f22
--- /dev/null
+++ b/Yatima/Compiler/GrinM.lean
@@ -0,0 +1,53 @@
+import Yatima.Compiler.Grin
+
+open Lean.Compiler.LCNF
+
+namespace Yatima.Grin
+
+-- The Grin compiler monad
+structure GrinEnv where
+  varKind : Lean.NameMap VarKind
+  env : Lean.Environment
+
+structure GrinState where
+  bindings : Lean.NameMap Binding
+  visited  : Lean.NameSet
+  ngen     : Lean.NameGenerator
+  deriving Inhabited
+
+abbrev GrinM := ReaderT GrinEnv $ EStateM String GrinState
+
+instance : Lean.MonadNameGenerator GrinM where
+  getNGen := return (← get).ngen
+  setNGen ngen := modify fun s => { s with ngen := ngen }
+
+def visit (name : Lean.Name) : GrinM Unit :=
+  modify fun s => { s with visited := s.visited.insert name }
+
+@[inline] def isVisited (n : Lean.Name) : GrinM Bool :=
+  return (← get).visited.contains n
+
+@[inline] def varKind (n : Lean.FVarId) : GrinM VarKind := do
+  match (← read).varKind.find? n.name with
+  | some kind => pure kind
+  | none => throw "Unknown variable"
+
+@[inline] def getBinding (n : Lean.FVarId) : GrinM Binding := do
+  match (← get).bindings.find? n.name with
+  | some binding => pure binding
+  | none => throw "Unknown variable"
+
+@[inline] def addBinding (n : Lean.FVarId) (binding : Binding) : GrinM Unit :=
+  modify (fun state => { state with bindings := state.bindings.insert n.name binding })
+
+def GrinM.run (env : GrinEnv) (s : GrinState) (m : GrinM α) :
+    EStateM.Result String GrinState α :=
+  m env |>.run s
+
+def getDecl (declName : Lean.Name) : GrinM Decl := do
+  let env := (← read).env
+  let some decl := getDeclCore? env monoExt declName
+    | throw s!"environment does not contain {declName}"
+  pure decl
+
+end Yatima.Grin
diff --git a/Yatima/Compiler/Yul.lean b/Yatima/Compiler/Yul.lean
new file mode 100644
index 00000000..0acee701
--- /dev/null
+++ b/Yatima/Compiler/Yul.lean
@@ -0,0 +1,203 @@
+import Init.Data.Repr
+import YatimaStdLib.NonEmpty
+
+-- This is based on Yul's specification https://docs.soliditylang.org/en/v0.8.17/yul.html#specification-of-yul
+namespace Yul
+
+-- Yul currently only supports the u256 type, but other types might be added in the future
+inductive PrimType where
+| u256
+
+abbrev Identifier := String
+structure TypedIdentifier where
+  identifier : Identifier
+  type       : Option PrimType
+
+inductive Literal where
+-- Actually it should be a u256
+| number : Option PrimType → Nat → Literal
+| string : Option PrimType → String → Literal
+| true   : Option PrimType → Literal
+| false  : Option PrimType → Literal
+
+inductive Expression where
+| functionCall : Identifier → List Expression → Expression
+| identifier   : Identifier → Expression
+| literal      : Literal → Expression
+
+mutual
+
+inductive Block where
+| mk : List Statement → Block
+
+inductive Switch where
+| case    : Expression → NEList (Literal × Block) → Option Block → Switch
+| default : Expression → Block → Switch
+
+inductive Statement where
+| block               : Block → Statement
+| functionDefinition  : Identifier → List TypedIdentifier → List TypedIdentifier → Block → Statement
+| variableDeclaration : NEList TypedIdentifier → Option Expression → Statement
+| assignment          : NEList Identifier → Expression → Statement
+| «if»                : Expression → Block → Statement
+| expression          : Expression → Statement
+| switch              : Switch → Statement
+| forLoop             : Block → Expression → Block → Block → Statement
+| «break»             : Statement
+| «continue»          : Statement
+| leave               : Statement
+
+end
+
+abbrev StringLiteral := String
+abbrev HexLiteral := Nat
+
+inductive Data where
+| str : StringLiteral → StringLiteral → Data
+| hex : StringLiteral → HexLiteral → Data
+
+inductive Object where
+| object : StringLiteral → Block → List (Sum Object Data) → Object
+
+abbrev Code := String
+def Code.inc (code : Code) : Code := "    " ++ code
+
+def PrimType.toCode : PrimType → Code
+| .u256 => "u256"
+
+def Identifier.toCode (id : Identifier) : Code := id
+
+def TypedIdentifier.toCode (id : TypedIdentifier) : Code :=
+  match id.type with
+  | none => id.identifier
+  | some type => id.identifier ++ " : " ++ type.toCode
+
+def Literal.toCode (lit : Literal) : Code :=
+  let (typ, lit) := match lit with
+    | .true typ => (typ, "true")
+    | .false typ => (typ, "false")
+    | .string typ str => (typ, s!"\"{str}\"")
+    | .number typ num => (typ, s!"{num}")
+  match typ with
+  | none => lit
+  | some typ => lit ++ " : " ++ typ.toCode
+
+-- Should not be partial functions, but Lean fails to prove termination
+partial def Expression.toCode (alreadyIndented : Bool) (indent : Code) (expr : Expression) : Code :=
+  let firstIndent := if alreadyIndented then "" else indent
+  match expr with
+  | .functionCall name args =>
+    let indent' := indent.inc
+    let args := match args with
+      | .nil => "()"
+      | .cons arg args' =>
+        args'.foldr
+          (fun arg' acc => ", " ++ Expression.toCode true indent' arg' ++ acc)
+          ("(" ++ arg.toCode true indent')
+        ++ ")"
+    firstIndent ++ name ++ args
+  | .identifier   name => firstIndent ++ name
+  | .literal lit => firstIndent ++ lit.toCode
+
+mutual
+
+partial def Block.toCode (alreadyIndented : Bool) (indent : Code) : Block → Code
+| .mk statements =>
+  let firstIndent := if alreadyIndented then "" else indent
+  let left := firstIndent ++ "{\n"
+  let inner := statements.foldr
+    (fun statement acc => Statement.toCode indent.inc statement ++ "\n" ++ acc)
+    ""
+  let right := indent ++ "}"
+  left ++ inner ++ right
+
+partial def Statement.toCode (indent : Code) : Statement → Code
+| .block block => block.toCode false indent
+| .functionDefinition  name args rets body =>
+  let header := indent ++ "function " ++ name.toCode
+  let args := match args with
+    | .nil => "()"
+    | .cons arg args' =>
+      args'.foldr
+        (fun arg' acc => ", " ++ TypedIdentifier.toCode arg' ++ acc)
+        ("(" ++ arg.toCode)
+      ++ ")"
+  let rets := match rets with
+    | .nil => ""
+    | .cons ret rets' =>
+      rets'.foldr
+        (fun ret' acc => ", " ++ TypedIdentifier.toCode ret' ++ acc)
+        ("-> " ++ ret.toCode)
+  let body := body.toCode true indent.inc
+  header ++ args ++ rets ++ body
+| .variableDeclaration names expr =>
+  let firstVar := indent ++ "let " ++ names.head.toCode
+  let otherVars := names.tail.foldr (fun name acc => ", " ++ name.toCode ++ acc) ""
+  match expr with
+  | none => firstVar ++ otherVars
+  | some expr => firstVar ++ otherVars ++ " := " ++ expr.toCode true indent.inc
+| .assignment          names expr =>
+  let firstVar := indent ++ names.head.toCode
+  let otherVars := names.tail.foldr (fun name acc => ", " ++ name.toCode ++ acc) ""
+  firstVar ++ otherVars ++ " := " ++ expr.toCode true indent.inc
+| .«if»                expr block =>
+  let indent' := indent.inc
+  let ifPart := indent ++ "if " ++ expr.toCode true indent'
+  let inner  := block.toCode true indent'
+  ifPart ++ inner
+| .expression          expr => expr.toCode false indent
+| .switch              switch => switch.toCode indent
+| .forLoop             init expr inc body =>
+  let indent' := indent.inc
+  let forPart := indent ++ "for " ++
+    init.toCode true indent' ++
+    expr.toCode true indent' ++
+    inc.toCode true indent'
+  let inner := body.toCode true indent'
+  forPart ++ inner
+| .«break»             => indent ++ "break"
+| .«continue»          => indent ++ "continue"
+| .leave               => indent ++ "leave"
+
+partial def Switch.toCode (indent : Code) : Switch → Code
+| .case expr caseList block? =>
+  let indent' := indent.inc
+  let header := indent ++ "switch " ++ expr.toCode true indent' ++ "\n"
+  let cases := caseList.toList.foldr
+    (fun (lit, block) acc => indent ++ "case " ++ lit.toCode ++ block.toCode true indent' ++ acc) ""
+  let default := match block? with
+    | none => ""
+    | some block => indent ++ "default " ++ block.toCode true indent'
+  header ++ cases ++ default
+| .default expr block =>
+  let indent' := indent.inc
+  let header := indent ++ "switch " ++ expr.toCode true indent' ++ "\n"
+  let default := indent ++ "default " ++ block.toCode true indent'
+  header ++ default
+
+end
+
+def HexLiteral.toCode (hex : HexLiteral) : Code :=
+  let base := 16
+  let num := (base.toDigits hex).asString
+  s!"hex\"{num}\""
+
+def StringLiteral.toCode (str : StringLiteral) : Code :=
+  s!"\"{str}\""
+
+def Data.toCode : Data → Code
+| .hex name hexLit => "data " ++ name.toCode ++ hexLit.toCode
+| .str name strLit => "data " ++ name.toCode ++ strLit.toCode
+
+partial def Object.toCode (indent : Code) : Object → Code
+| .object name code args =>
+  let objHeader := indent ++ "object " ++ name.toCode ++ " {\n"
+  let indent' := indent.inc
+  let codeHeader := indent' ++ "code " ++ name.toCode ++ code.toCode true indent'.inc
+  let argToCode arg := match arg with
+  | .inl obj => obj.toCode indent'
+  | .inr data => indent' ++ data.toCode
+  let args := args.foldr (fun arg acc => "\n" ++ argToCode arg ++ acc) "\n"
+  objHeader ++ codeHeader ++ args ++ indent ++ "}"
+
+end Yul
diff --git a/lake-manifest.json b/lake-manifest.json
index 52cb5e0d..51d8dd77 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/yatima-inc/YatimaStdLib.lean",
     "subDir?": null,
-    "rev": "704823e421b333ea9960347e305c60f654618422",
+    "rev": "b3084d5fb020975555dabe507e6a4db659b0733d",
     "name": "YatimaStdLib",
-    "inputRev?": "704823e421b333ea9960347e305c60f654618422"}},
+    "inputRev?": "b3084d5fb020975555dabe507e6a4db659b0733d"}},
   {"git":
    {"url": "https://github.com/yatima-inc/Lurk.lean",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index f89a1ad2..4ad05ddc 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -18,7 +18,7 @@ require LSpec from git
   "https://github.com/yatima-inc/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
 
 require YatimaStdLib from git
-  "https://github.com/yatima-inc/YatimaStdLib.lean" @ "704823e421b333ea9960347e305c60f654618422"
+  "https://github.com/yatima-inc/YatimaStdLib.lean" @ "b3084d5fb020975555dabe507e6a4db659b0733d"
 
 require Cli from git
   "https://github.com/yatima-inc/Cli.lean" @ "b76218dbaa20ac51cf4e6789407e42b76dd3061f"