diff --git a/Juvix.lean b/Juvix.lean
index a01e0fb..62a9846 100644
--- a/Juvix.lean
+++ b/Juvix.lean
@@ -1,3 +1,3 @@
 -- This module serves as the root of the `Juvix` library.
 -- Import modules here that should be built as part of the library.
-import Juvix.Basic
+import Juvix.Core.Main
diff --git a/Juvix/Basic.lean b/Juvix/Basic.lean
deleted file mode 100644
index 99415d9..0000000
--- a/Juvix/Basic.lean
+++ /dev/null
@@ -1 +0,0 @@
-def hello := "world"
diff --git a/Juvix/Core/Main.lean b/Juvix/Core/Main.lean
new file mode 100644
index 0000000..7f1ff5d
--- /dev/null
+++ b/Juvix/Core/Main.lean
@@ -0,0 +1,3 @@
+
+import Juvix.Core.Main.Language
+import Juvix.Core.Main.Semantics
diff --git a/Juvix/Core/Main/Language.lean b/Juvix/Core/Main/Language.lean
new file mode 100644
index 0000000..a7dd43a
--- /dev/null
+++ b/Juvix/Core/Main/Language.lean
@@ -0,0 +1,3 @@
+
+import Juvix.Core.Main.Language.Base
+import Juvix.Core.Main.Language.Value
diff --git a/Juvix/Core/Main/Language/Base.lean b/Juvix/Core/Main/Language/Base.lean
new file mode 100644
index 0000000..74032e4
--- /dev/null
+++ b/Juvix/Core/Main/Language/Base.lean
@@ -0,0 +1,40 @@
+
+namespace Juvix.Core.Main
+
+abbrev Name : Type := String
+
+inductive Constant : Type where
+  | int : Int → Constant
+  | string : String → Constant
+  deriving Inhabited, DecidableEq
+
+inductive BuiltinOp : Type where
+  | add_int : BuiltinOp
+  | sub_int : BuiltinOp
+  | mul_int : BuiltinOp
+  | div_int : BuiltinOp
+  deriving Inhabited, DecidableEq
+
+mutual
+  inductive Expr : Type where
+    | var : Nat → Expr
+    | ident : Name → Expr
+    | const : Constant → Expr
+    | app : Expr → Expr → Expr
+    | builtin_app : (oper : BuiltinOp) → (args : List Expr) → Expr
+    | constr_app : (constr : Name) → (args : List Expr) → Expr
+    | lambda : (body : Expr) → Expr
+    | let : (value : Expr) → (body : Expr) → Expr
+    | case : (value : Expr) → (branches : List CaseBranch) → Expr
+    | unit : Expr
+    deriving Inhabited
+
+  structure CaseBranch where
+    constr : Name
+    body : Expr
+end
+
+structure Program where
+  defs : List Expr
+
+end Juvix.Core.Main
diff --git a/Juvix/Core/Main/Language/Value.lean b/Juvix/Core/Main/Language/Value.lean
new file mode 100644
index 0000000..dd5f8a6
--- /dev/null
+++ b/Juvix/Core/Main/Language/Value.lean
@@ -0,0 +1,15 @@
+
+import Juvix.Core.Main.Language.Base
+
+namespace Juvix.Core.Main
+
+inductive Value : Type where
+  | const : Constant → Value
+  | constr_app : (constr : Name) → (args : List Value) → Value
+  | closure : (ctx : List Value) → (value : Expr) → Value
+  | unit : Value
+  deriving Inhabited
+
+abbrev Context : Type := List Value
+
+end Juvix.Core.Main
diff --git a/Juvix/Core/Main/Semantics.lean b/Juvix/Core/Main/Semantics.lean
new file mode 100644
index 0000000..0cb9714
--- /dev/null
+++ b/Juvix/Core/Main/Semantics.lean
@@ -0,0 +1,11 @@
+
+import Juvix.Core.Main.Language
+
+namespace Juvix.Core.Main
+
+def f : Expr -> Expr := λ e =>
+  match e with
+  | Expr.lambda (body := e) => e
+  | _ => Expr.lambda (body := e)
+
+end Juvix.Core.Main
diff --git a/Juvix/Core/Stored/Language.lean b/Juvix/Core/Stored/Language.lean
new file mode 100644
index 0000000..e69de29
diff --git a/Juvix/Core/Stored/Semantics.lean b/Juvix/Core/Stored/Semantics.lean
new file mode 100644
index 0000000..e69de29
diff --git a/Juvix/Core/Stripped/Language.lean b/Juvix/Core/Stripped/Language.lean
new file mode 100644
index 0000000..e69de29
diff --git a/Juvix/Core/Stripped/Semantics.lean b/Juvix/Core/Stripped/Semantics.lean
new file mode 100644
index 0000000..e69de29