diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,7 @@
+Copyright 2021-present Junyoung Clare Jang
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,1 @@
+# LambdaCube
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/lambda-cube.cabal b/lambda-cube.cabal
new file mode 100644
--- /dev/null
+++ b/lambda-cube.cabal
@@ -0,0 +1,180 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.34.4.
+--
+-- see: https://github.com/sol/hpack
+
+name:           lambda-cube
+version:        0.1.0.0
+synopsis:       Haskell implementation of (some of) lambda cube calculi
+description:    Haskell implementation of the following 4 lambda calculi:
+                1. Simply typed lambda calculus
+                2. System F
+                3. System F omega underbar
+                4. System F omega
+category:       Utilities
+homepage:       https://github.com/Ailrun/LambdaCube#readme
+bug-reports:    https://github.com/Ailrun/LambdaCube/issues
+author:         Junyoung Clare Jang
+maintainer:     jjc9310@gmail.com
+copyright:      2021 Junyoung Clare Jang
+license:        MIT
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+
+source-repository head
+  type: git
+  location: https://github.com/Ailrun/LambdaCube
+
+library
+  exposed-modules:
+      LambdaCube.Common.Parser
+      LambdaCube.Common.PrettyPrinter
+      LambdaCube.STLC.Ast
+      LambdaCube.STLC.Elaborator
+      LambdaCube.STLC.Evaluator
+      LambdaCube.STLC.Normalizer
+      LambdaCube.STLC.Parser
+      LambdaCube.STLC.PrettyPrinter
+      LambdaCube.STLC.TH
+      LambdaCube.STLC.TypeChecker
+      LambdaCube.SystemF.Ast
+      LambdaCube.SystemF.Elaborator
+      LambdaCube.SystemF.Evaluator
+      LambdaCube.SystemF.Normalizer
+      LambdaCube.SystemF.Parser
+      LambdaCube.SystemF.PrettyPrinter
+      LambdaCube.SystemF.TH
+      LambdaCube.SystemF.TypeChecker
+      LambdaCube.SystemFw.Ast
+      LambdaCube.SystemFw.Elaborator
+      LambdaCube.SystemFw.Evaluator
+      LambdaCube.SystemFw.Normalizer
+      LambdaCube.SystemFw.Parser
+      LambdaCube.SystemFw.PrettyPrinter
+      LambdaCube.SystemFw.TH
+      LambdaCube.SystemFw.TypeChecker
+      LambdaCube.SystemFw_.Ast
+      LambdaCube.SystemFw_.Elaborator
+      LambdaCube.SystemFw_.Evaluator
+      LambdaCube.SystemFw_.Normalizer
+      LambdaCube.SystemFw_.Parser
+      LambdaCube.SystemFw_.PrettyPrinter
+      LambdaCube.SystemFw_.TH
+      LambdaCube.SystemFw_.TypeChecker
+  other-modules:
+      Paths_lambda_cube
+  hs-source-dirs:
+      src
+  default-extensions:
+      BangPatterns
+      BinaryLiterals
+      ConstrainedClassMethods
+      ConstraintKinds
+      DeriveDataTypeable
+      DeriveFoldable
+      DeriveFunctor
+      DeriveGeneric
+      DeriveLift
+      DeriveTraversable
+      DerivingStrategies
+      EmptyCase
+      EmptyDataDecls
+      EmptyDataDeriving
+      ExistentialQuantification
+      ExplicitForAll
+      FlexibleContexts
+      FlexibleInstances
+      ForeignFunctionInterface
+      GADTSyntax
+      GeneralizedNewtypeDeriving
+      HexFloatLiterals
+      ImportQualifiedPost
+      InstanceSigs
+      KindSignatures
+      LambdaCase
+      MultiParamTypeClasses
+      NamedFieldPuns
+      NamedWildCards
+      NumericUnderscores
+      PolyKinds
+      PostfixOperators
+      RankNTypes
+      RecordWildCards
+      ScopedTypeVariables
+      StandaloneDeriving
+      StandaloneKindSignatures
+      StarIsType
+      TupleSections
+      TypeApplications
+      TypeFamilies
+      TypeOperators
+      TypeSynonymInstances
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-deriving-strategies -Wmissing-home-modules -Wmonomorphism-restriction -Wpartial-fields -Wredundant-constraints -Wunused-type-patterns
+  build-depends:
+      base >=4.12 && <5
+    , megaparsec >=9.0.1 && <9.1
+    , template-haskell
+    , text
+  default-language: Haskell2010
+
+test-suite lambda-cube-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Paths_lambda_cube
+  hs-source-dirs:
+      test
+  default-extensions:
+      BangPatterns
+      BinaryLiterals
+      ConstrainedClassMethods
+      ConstraintKinds
+      DeriveDataTypeable
+      DeriveFoldable
+      DeriveFunctor
+      DeriveGeneric
+      DeriveLift
+      DeriveTraversable
+      DerivingStrategies
+      EmptyCase
+      EmptyDataDecls
+      EmptyDataDeriving
+      ExistentialQuantification
+      ExplicitForAll
+      FlexibleContexts
+      FlexibleInstances
+      ForeignFunctionInterface
+      GADTSyntax
+      GeneralizedNewtypeDeriving
+      HexFloatLiterals
+      ImportQualifiedPost
+      InstanceSigs
+      KindSignatures
+      LambdaCase
+      MultiParamTypeClasses
+      NamedFieldPuns
+      NamedWildCards
+      NumericUnderscores
+      PolyKinds
+      PostfixOperators
+      RankNTypes
+      RecordWildCards
+      ScopedTypeVariables
+      StandaloneDeriving
+      StandaloneKindSignatures
+      StarIsType
+      TupleSections
+      TypeApplications
+      TypeFamilies
+      TypeOperators
+      TypeSynonymInstances
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-deriving-strategies -Wmissing-home-modules -Wmonomorphism-restriction -Wpartial-fields -Wredundant-constraints -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      QuickCheck
+    , base
+    , hspec
+    , lambda-cube
+  default-language: Haskell2010
diff --git a/src/LambdaCube/Common/Parser.hs b/src/LambdaCube/Common/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/Common/Parser.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE OverloadedStrings #-}
+module LambdaCube.Common.Parser where
+
+import           Prelude              hiding (lex)
+
+import           Data.Text            (Text)
+import qualified Data.Text            as Text
+import           Data.Void            (Void)
+import           Text.Megaparsec
+import           Text.Megaparsec.Char
+
+type Parser = Parsec Void Text
+
+topParser :: Parser a -> Parser a
+topParser = between space eof
+
+parenthesized :: Parser a -> Parser a
+parenthesized = between openParenthesis closeParenthesis
+
+rightArrow, atsignBackslash :: Parser Text
+rightArrow = lex $ string "->"
+atsignBackslash = lex $ string "@\\"
+
+backslash, atsign, sharp, colon, dot, openParenthesis, closeParenthesis, exclamationMark, comma, asterisk :: Parser Char
+backslash        = lex $ char '\\'
+atsign           = lex $ char '@'
+sharp            = lex $ char '#'
+colon            = lex $ char ':'
+dot              = lex $ char '.'
+openParenthesis  = lex $ char '('
+closeParenthesis = lex $ char ')'
+exclamationMark  = lex $ char '!'
+comma            = lex $ char ','
+asterisk         = lex $ char '*'
+
+identifier :: Parser Text
+identifier = lex $ (Text.pack .) . (:) <$> letterChar <*> many alphaNumChar
+
+lex :: Parser a -> Parser a
+lex = (<* space)
diff --git a/src/LambdaCube/Common/PrettyPrinter.hs b/src/LambdaCube/Common/PrettyPrinter.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/Common/PrettyPrinter.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE OverloadedStrings #-}
+module LambdaCube.Common.PrettyPrinter where
+
+import           Data.Text (Text)
+import qualified Data.Text as Text
+
+wrapIfSpaced :: Bool -> [Text] -> Text
+wrapIfSpaced b = wrapIf b . spaced
+
+wrap :: Text -> Text
+wrap t = "(" <> t <> ")"
+
+wrapIf :: Bool -> Text -> Text
+wrapIf True  = wrap
+wrapIf False = id
+
+spaced :: [Text] -> Text
+spaced = Text.intercalate " "
diff --git a/src/LambdaCube/STLC/Ast.hs b/src/LambdaCube/STLC/Ast.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/STLC/Ast.hs
@@ -0,0 +1,39 @@
+module LambdaCube.STLC.Ast where
+
+import           Data.Text                  (Text)
+import           Language.Haskell.TH.Syntax (Lift)
+
+data ExtLCTerm
+  = ExtLCVar Text
+  | ExtLCLam Text LCType ExtLCTerm
+  | ExtLCApp ExtLCTerm ExtLCTerm
+  deriving stock (Eq, Show, Lift)
+infixl 6 `ExtLCApp`
+
+data LCType
+  = LCBase
+  | LCArr LCType LCType
+  deriving stock (Eq, Show, Lift)
+infixr 5 `LCArr`
+
+data LCTerm
+  = LCVar Int
+  | LCLam LCType LCTerm
+  | LCApp LCTerm LCTerm
+  deriving stock (Eq, Show, Lift)
+infixl 6 `LCApp`
+
+data LCValue
+  = LCValLam LCType LCTerm
+  deriving stock (Eq, Show, Lift)
+
+data LCNormalTerm
+  = LCNormLam LCType LCNormalTerm
+  | LCNormNeut LCNeutralTerm
+  deriving stock (Eq, Show, Lift)
+
+data LCNeutralTerm
+  = LCNeutVar Int
+  | LCNeutApp LCNeutralTerm LCNormalTerm
+  deriving stock (Eq, Show, Lift)
+infixl 6 `LCNeutApp`
diff --git a/src/LambdaCube/STLC/Elaborator.hs b/src/LambdaCube/STLC/Elaborator.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/STLC/Elaborator.hs
@@ -0,0 +1,16 @@
+module LambdaCube.STLC.Elaborator where
+
+import           Data.List           (elemIndex)
+import qualified Data.Text           as Text
+import           LambdaCube.STLC.Ast
+
+elaborate :: ExtLCTerm -> Either String LCTerm
+elaborate = go []
+  where
+    go l (ExtLCVar v)
+      | Just idx <- v `elemIndex` l
+      = Right $ LCVar idx
+      | otherwise
+      = Left $ "Variable " <> Text.unpack v <> " is not in scope"
+    go l (ExtLCLam v t b) = LCLam t <$> go (v : l) b
+    go l (ExtLCApp f a) = LCApp <$> go l f <*> go l a
diff --git a/src/LambdaCube/STLC/Evaluator.hs b/src/LambdaCube/STLC/Evaluator.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/STLC/Evaluator.hs
@@ -0,0 +1,23 @@
+module LambdaCube.STLC.Evaluator where
+
+import           LambdaCube.STLC.Ast
+
+liftLCValue :: LCValue -> LCTerm
+liftLCValue (LCValLam t b) = LCLam t b
+
+substituteValue :: Int -> LCValue -> LCTerm -> LCTerm
+substituteValue n v = go n
+  where
+    go m e@(LCVar l) = if m == l then liftLCValue v else e
+    go m (LCLam t b) = LCLam t $ go (m + 1) b
+    go m (LCApp f a) = go m f `LCApp` go m a
+
+evaluate :: LCTerm -> LCValue
+evaluate = go
+  where
+    go (LCVar _) = error "Did you really type check this?"
+    go (LCLam t b) = LCValLam t b
+    go (LCApp f a)
+      | LCValLam _ b <- go f
+      , v <- go a
+      = go $ substituteValue 0 v b
diff --git a/src/LambdaCube/STLC/Normalizer.hs b/src/LambdaCube/STLC/Normalizer.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/STLC/Normalizer.hs
@@ -0,0 +1,32 @@
+module LambdaCube.STLC.Normalizer where
+
+import           LambdaCube.STLC.Ast
+
+substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
+substituteNormal n nv = go n
+  where
+    go m (LCNormLam t b)   = LCNormLam t $ go (m + 1) b
+    go m (LCNormNeut neut) = substituteNeutral m nv neut
+
+substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
+substituteNeutral n nv = go n
+  where
+    go m e@(LCNeutVar l) = if m == l then nv else LCNormNeut e
+    go m (LCNeutApp f a) =
+      case go m f of
+        LCNormLam _ b   -> substituteNormal 0 a' b
+        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
+      where
+        a' = substituteNormal m nv a
+
+normalize :: LCTerm -> LCNormalTerm
+normalize = go
+  where
+    go (LCVar n) = LCNormNeut $ LCNeutVar n
+    go (LCLam t b) = LCNormLam t $ go b
+    go (LCApp f a) =
+      case go f of
+        LCNormLam t b   -> LCNormLam t $ substituteNormal 0 a' b
+        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
+      where
+        a' = go a
diff --git a/src/LambdaCube/STLC/Parser.hs b/src/LambdaCube/STLC/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/STLC/Parser.hs
@@ -0,0 +1,32 @@
+module LambdaCube.STLC.Parser where
+
+import           Data.Foldable            (Foldable (foldl'))
+import           Data.Functor             (($>))
+import           LambdaCube.Common.Parser
+import           LambdaCube.STLC.Ast
+import           Text.Megaparsec
+
+pTopLC :: Parser ExtLCTerm
+pTopLC = topParser pLC
+
+pLC :: Parser ExtLCTerm
+pLC = pLam <|> pApp
+
+pLam :: Parser ExtLCTerm
+pLam =
+  ExtLCLam
+  <$> (backslash *> identifier)
+  <*> (colon *> pType)
+  <*> (dot *> pLC)
+
+pApp :: Parser ExtLCTerm
+pApp = foldl' ExtLCApp <$> pATerm <*> many pATerm
+
+pATerm :: Parser ExtLCTerm
+pATerm = (ExtLCVar <$> identifier) <|> parenthesized pLC
+
+pType :: Parser LCType
+pType = foldr1 LCArr <$> sepBy1 pAType rightArrow
+
+pAType :: Parser LCType
+pAType = (sharp $> LCBase) <|> parenthesized pType
diff --git a/src/LambdaCube/STLC/PrettyPrinter.hs b/src/LambdaCube/STLC/PrettyPrinter.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/STLC/PrettyPrinter.hs
@@ -0,0 +1,31 @@
+{- |
+  TODO: Use real pretty printer library
+-}
+{-# LANGUAGE OverloadedStrings #-}
+module LambdaCube.STLC.PrettyPrinter where
+
+import           Data.Text                       (Text)
+import qualified Data.Text                       as Text
+import           LambdaCube.Common.PrettyPrinter
+import           LambdaCube.STLC.Ast
+
+prettyType :: LCType -> Text
+prettyType = prettyTypePrec 0
+
+prettyTerm :: LCTerm -> Text
+prettyTerm = prettyTermPrec 0
+
+prettyTypePrec :: Int -> LCType -> Text
+prettyTypePrec = go
+  where
+    go _ LCBase      = "#"
+    go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
+
+prettyTermPrec :: Int -> LCTerm -> Text
+prettyTermPrec = go
+  where
+    pTP = prettyTypePrec
+
+    go _ (LCVar n)   = Text.pack $ show n
+    go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
+    go p (LCApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
diff --git a/src/LambdaCube/STLC/TH.hs b/src/LambdaCube/STLC/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/STLC/TH.hs
@@ -0,0 +1,43 @@
+module LambdaCube.STLC.TH where
+
+import           Control.Monad              ((<=<))
+import qualified Data.Text                  as Text
+import           LambdaCube.STLC.Ast
+import           LambdaCube.STLC.Elaborator
+import           LambdaCube.STLC.Parser
+import           Language.Haskell.TH.Quote  (QuasiQuoter (..))
+import           Language.Haskell.TH.Syntax (Loc (loc_start), Q, lift, location)
+import qualified Text.Megaparsec            as P
+import qualified Text.Megaparsec.Error      as PE
+
+stlc :: QuasiQuoter
+stlc =
+  QuasiQuoter
+    { quoteExp = lift <=< stlcQuoteExp
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+stlcQuoteExp :: String -> Q ExtLCTerm
+stlcQuoteExp str = do
+  l <- location
+  case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
+    Right e  -> pure e
+    Left err -> fail $ PE.errorBundlePretty err
+
+elaboratedStlc :: QuasiQuoter
+elaboratedStlc =
+  QuasiQuoter
+    { quoteExp = lift <=< elaboratedStlcQuoteExp
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+elaboratedStlcQuoteExp :: String -> Q LCTerm
+elaboratedStlcQuoteExp str = do
+  e <- stlcQuoteExp str
+  case elaborate e of
+    Right e' -> pure e'
+    Left err -> fail err
diff --git a/src/LambdaCube/STLC/TypeChecker.hs b/src/LambdaCube/STLC/TypeChecker.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/STLC/TypeChecker.hs
@@ -0,0 +1,17 @@
+module LambdaCube.STLC.TypeChecker where
+
+import           Data.List           (uncons)
+import           LambdaCube.STLC.Ast
+
+infer :: LCTerm -> Maybe LCType
+infer = go []
+  where
+    go l (LCVar n) = fmap fst . uncons $ drop n l
+    go l (LCLam t b) = LCArr t <$> go (t : l) b
+    go l (LCApp f a)
+      | Just (LCArr at' rt) <- go l f
+      , Just at <- go l a
+      , at == at'
+      = Just rt
+      | otherwise
+      = Nothing
diff --git a/src/LambdaCube/SystemF/Ast.hs b/src/LambdaCube/SystemF/Ast.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemF/Ast.hs
@@ -0,0 +1,59 @@
+module LambdaCube.SystemF.Ast where
+
+import           Data.Text                  (Text)
+import           Language.Haskell.TH.Syntax (Lift)
+
+data ExtLCType
+  = ExtLCBase
+  | ExtLCTVar Text
+  | ExtLCArr ExtLCType ExtLCType
+  | ExtLCUniv Text ExtLCType
+  deriving stock (Eq, Show, Lift)
+infixr 5 `ExtLCArr`
+
+data ExtLCTerm
+  = ExtLCVar Text
+  | ExtLCLam Text ExtLCType ExtLCTerm
+  | ExtLCApp ExtLCTerm ExtLCTerm
+  | ExtLCTLam Text ExtLCTerm
+  | ExtLCTApp ExtLCTerm ExtLCType
+  deriving stock (Eq, Show, Lift)
+infixl 6 `ExtLCApp`
+infixl 6 `ExtLCTApp`
+
+data LCType
+  = LCBase
+  | LCTVar Int
+  | LCArr LCType LCType
+  | LCUniv LCType
+  deriving stock (Eq, Show, Lift)
+infixr 5 `LCArr`
+
+data LCTerm
+  = LCVar Int
+  | LCLam LCType LCTerm
+  | LCApp LCTerm LCTerm
+  | LCTLam LCTerm
+  | LCTApp LCTerm LCType
+  deriving stock (Eq, Show, Lift)
+infixl 6 `LCApp`
+infixl 6 `LCTApp`
+
+data LCValue
+  = LCValLam LCType LCTerm
+  | LCValTLam LCTerm
+  deriving stock (Eq, Show, Lift)
+
+data LCNormalTerm
+  = LCNormLam LCType LCNormalTerm
+  | LCNormTLam LCNormalTerm
+  | LCNormNeut LCNeutralTerm
+  deriving stock (Eq, Show, Lift)
+
+data LCNeutralTerm
+  = LCNeutVar Int
+  | LCNeutApp LCNeutralTerm LCNormalTerm
+  | LCNeutTApp LCNeutralTerm LCType
+  deriving stock (Eq, Show, Lift)
+infixl 6 `LCNeutApp`
+infixl 6 `LCNeutTApp`
diff --git a/src/LambdaCube/SystemF/Elaborator.hs b/src/LambdaCube/SystemF/Elaborator.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemF/Elaborator.hs
@@ -0,0 +1,31 @@
+module LambdaCube.SystemF.Elaborator where
+
+import           Data.List              (elemIndex)
+import           Data.Text              (Text)
+import qualified Data.Text              as Text
+import           LambdaCube.SystemF.Ast
+
+elaborate :: ExtLCTerm -> Either String LCTerm
+elaborate = go [] []
+  where
+    go _  vl (ExtLCVar x)
+      | Just n <- x `elemIndex` vl
+      = Right $ LCVar n
+      | otherwise
+      = Left $ "Term variable " <> Text.unpack x <> " is not in scope"
+    go tl vl (ExtLCLam x t b) = LCLam <$> typeElaborate tl t <*> go tl (x : vl) b
+    go tl vl (ExtLCApp f a) = LCApp <$> go tl vl f <*> go tl vl a
+    go tl vl (ExtLCTLam x b) = LCTLam <$> go (x : tl) vl b
+    go tl vl (ExtLCTApp f t) = LCTApp <$> go tl vl f <*> typeElaborate tl t
+
+typeElaborate :: [Text] -> ExtLCType -> Either String LCType
+typeElaborate = go
+  where
+    go _ ExtLCBase = Right LCBase
+    go l (ExtLCTVar x)
+      | Just n <- x `elemIndex` l
+      = Right $ LCTVar n
+      | otherwise
+      = Left  $ "Type variable " <> Text.unpack x <> " is not in scope"
+    go l (ExtLCArr a b) = LCArr <$> go l a <*> go l b
+    go l (ExtLCUniv x a) = LCUniv <$> go (x : l) a
diff --git a/src/LambdaCube/SystemF/Evaluator.hs b/src/LambdaCube/SystemF/Evaluator.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemF/Evaluator.hs
@@ -0,0 +1,35 @@
+module LambdaCube.SystemF.Evaluator where
+
+import           LambdaCube.SystemF.Ast
+import           LambdaCube.SystemF.TypeChecker (substituteType)
+
+liftLCValue :: LCValue -> LCTerm
+liftLCValue (LCValLam t b) = LCLam t b
+liftLCValue (LCValTLam b)  = LCTLam b
+
+substitute :: Int -> LCValue -> LCTerm -> LCTerm
+substitute n v = go n
+  where
+    go m e@(LCVar l)  = if m == l then liftLCValue v else e
+    go m (LCLam t b)  = LCLam t $ go (m + 1) b
+    go m (LCApp f a)  = go m f `LCApp` go m a
+    go m (LCTLam b)   = LCTLam $ go m b
+    go m (LCTApp f t) = go m f `LCTApp` t
+
+evaluate :: LCTerm -> LCValue
+evaluate = go
+  where
+    go (LCVar _) = error "Did you really type check this?"
+    go (LCLam t b) = LCValLam t b
+    go (LCApp f a)
+      | LCValLam _ b <- go f
+      , v <- go a
+      = go $ substitute 0 v b
+      | otherwise
+      = error "Did you really type check this?"
+    go (LCTLam b) = LCValTLam b
+    go (LCTApp f t)
+      | LCValTLam b <- go f
+      = go $ substituteType 0 t b
+      | otherwise
+      = error "Did you really type check this?"
diff --git a/src/LambdaCube/SystemF/Normalizer.hs b/src/LambdaCube/SystemF/Normalizer.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemF/Normalizer.hs
@@ -0,0 +1,75 @@
+module LambdaCube.SystemF.Normalizer where
+
+import           LambdaCube.SystemF.Ast
+import           LambdaCube.SystemF.TypeChecker (substituteTypeInType)
+
+substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
+substituteNormal n v = go n
+  where
+    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b
+    go m (LCNormTLam b)  = LCNormTLam $ go m b
+    go m (LCNormNeut nt) = substituteNeutral m v nt
+
+substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
+substituteNeutral n v = go n
+  where
+    go m e@(LCNeutVar l)
+      | m == l = v
+      | otherwise = LCNormNeut e
+    go m (LCNeutApp f a) =
+      case go m f of
+        LCNormLam _ b -> substituteNormal 0 a' b
+        LCNormTLam _  -> error "Did you really type check this?"
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
+      where
+        a' = substituteNormal m v a
+    go m (LCNeutTApp f t) =
+      case go m f of
+        LCNormLam _ _ -> error "Did you really type check this?"
+        LCNormTLam b  -> substituteTypeNormal 0 t b
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t
+
+substituteTypeNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm
+substituteTypeNormal n v = go n
+  where
+    go m (LCNormLam t b) = LCNormLam (substituteTypeInType m v t) $ go m b
+    go m (LCNormTLam b)  = LCNormTLam $ go (m + 1) b
+    go m (LCNormNeut nt) = substituteTypeNeutral m v nt
+
+substituteTypeNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm
+substituteTypeNeutral n v = go n
+  where
+    go _ e@(LCNeutVar _) = LCNormNeut e
+    go m (LCNeutApp f a) =
+      case go m f of
+        LCNormLam _ b -> substituteNormal 0 a' b
+        LCNormTLam _  -> error "Did you really type check this?"
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
+      where
+        a' = substituteTypeNormal m v a
+    go m (LCNeutTApp f t) =
+      case go m f of
+        LCNormLam _ _ -> error "Did you really type check this?"
+        LCNormTLam b  -> substituteTypeNormal 0 t' b
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t'
+      where
+        t' = substituteTypeInType m v t
+
+normalize :: LCTerm -> LCNormalTerm
+normalize = go
+  where
+    go (LCVar n) = LCNormNeut $ LCNeutVar n
+    go (LCLam t b) = LCNormLam t $ go b
+    go (LCTLam b) = LCNormTLam $ go b
+    go (LCApp f a) =
+      case go f of
+        LCNormLam _ b   -> substituteNormal 0 a' b
+        LCNormTLam _    -> error "Did you really type check this?"
+        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
+      where
+        a' = go a
+    go (LCTApp f t) =
+      case go f of
+        LCNormLam _ _   -> error "Did you really type check this?"
+        LCNormTLam b    -> substituteTypeNormal 0 t b
+        LCNormNeut neut -> LCNormNeut $ neut `LCNeutTApp` t
diff --git a/src/LambdaCube/SystemF/Parser.hs b/src/LambdaCube/SystemF/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemF/Parser.hs
@@ -0,0 +1,56 @@
+module LambdaCube.SystemF.Parser where
+
+import           Data.Foldable            (Foldable (foldl'))
+import           Data.Function            ((&))
+import           Data.Functor             (($>))
+import           Data.Maybe               (isJust)
+import           LambdaCube.Common.Parser
+import           LambdaCube.SystemF.Ast
+import           Text.Megaparsec
+
+pTopLC :: Parser ExtLCTerm
+pTopLC = topParser pLC
+
+pLC :: Parser ExtLCTerm
+pLC = pTLam <|> pLam <|> pApp
+
+pTLam :: Parser ExtLCTerm
+pTLam =
+  ExtLCTLam
+  <$> (atsignBackslash *> identifier <* colon <* asterisk)
+  <*> (dot *> pLC)
+
+pLam :: Parser ExtLCTerm
+pLam =
+  ExtLCLam
+  <$> (backslash *> identifier)
+  <*> (colon *> pType)
+  <*> (dot *> pLC)
+
+pApp :: Parser ExtLCTerm
+pApp = foldl' (&) <$> pATerm <*> many pAppArg
+
+pAppArg :: Parser (ExtLCTerm -> ExtLCTerm)
+pAppArg = do
+  isType <- isJust <$> optional atsign
+  if isType
+    then flip ExtLCTApp <$> pAType
+    else flip ExtLCApp <$> pATerm
+
+pATerm :: Parser ExtLCTerm
+pATerm = (ExtLCVar <$> identifier) <|> parenthesized pLC
+
+pType :: Parser ExtLCType
+pType = pUniv <|> pArr
+
+pUniv :: Parser ExtLCType
+pUniv =
+  ExtLCUniv
+  <$> (exclamationMark *> identifier <* colon <* asterisk)
+  <*> (comma *> pType)
+
+pArr :: Parser ExtLCType
+pArr = foldr1 ExtLCArr <$> sepBy1 pAType rightArrow
+
+pAType :: Parser ExtLCType
+pAType = (sharp $> ExtLCBase) <|> (ExtLCTVar <$> identifier) <|> parenthesized pType
diff --git a/src/LambdaCube/SystemF/PrettyPrinter.hs b/src/LambdaCube/SystemF/PrettyPrinter.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemF/PrettyPrinter.hs
@@ -0,0 +1,35 @@
+{- |
+  TODO: Use real pretty printer library
+-}
+{-# LANGUAGE OverloadedStrings #-}
+module LambdaCube.SystemF.PrettyPrinter where
+
+import           Data.Text                       (Text)
+import qualified Data.Text                       as Text
+import           LambdaCube.Common.PrettyPrinter
+import           LambdaCube.SystemF.Ast
+
+prettyType :: LCType -> Text
+prettyType = prettyTypePrec 0
+
+prettyTerm :: LCTerm -> Text
+prettyTerm = prettyTermPrec 0
+
+prettyTypePrec :: Int -> LCType -> Text
+prettyTypePrec = go
+  where
+    go _ LCBase      = "#"
+    go _ (LCTVar i)  = Text.pack $ show i
+    go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
+    go p (LCUniv b)  = wrapIfSpaced (p > 0) ["! : * ,", go 0 b]
+
+prettyTermPrec :: Int -> LCTerm -> Text
+prettyTermPrec = go
+  where
+    pTP = prettyTypePrec
+
+    go _ (LCVar i)    = Text.pack $ show i
+    go p (LCLam t b)  = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
+    go p (LCApp f a)  = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
+    go p (LCTLam b)   = wrapIfSpaced (p > 0) ["@\\ : * .", go 0 b]
+    go p (LCTApp f t) = wrapIfSpaced (p > 1) [go 1 f, "@" <> pTP 1 t]
diff --git a/src/LambdaCube/SystemF/TH.hs b/src/LambdaCube/SystemF/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemF/TH.hs
@@ -0,0 +1,44 @@
+module LambdaCube.SystemF.TH where
+
+import           Control.Monad                 ((<=<))
+import qualified Data.Text                     as Text
+import           LambdaCube.SystemF.Ast
+import           LambdaCube.SystemF.Elaborator
+import           LambdaCube.SystemF.Parser
+import           Language.Haskell.TH.Quote     (QuasiQuoter (..))
+import           Language.Haskell.TH.Syntax    (Loc (loc_start), Q, lift,
+                                                location)
+import qualified Text.Megaparsec               as P
+import qualified Text.Megaparsec.Error         as PE
+
+systemF :: QuasiQuoter
+systemF =
+  QuasiQuoter
+    { quoteExp = lift <=< systemFQuoteExp
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+systemFQuoteExp :: String -> Q ExtLCTerm
+systemFQuoteExp str = do
+  l <- location
+  case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
+    Right e  -> pure e
+    Left err -> fail $ PE.errorBundlePretty err
+
+elaboratedSystemF :: QuasiQuoter
+elaboratedSystemF =
+  QuasiQuoter
+    { quoteExp = lift <=< elaboratedSystemFQuoteExp
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+elaboratedSystemFQuoteExp :: String -> Q LCTerm
+elaboratedSystemFQuoteExp str = do
+  e <- systemFQuoteExp str
+  case elaborate e of
+    Right e' -> pure e'
+    Left err -> fail err
diff --git a/src/LambdaCube/SystemF/TypeChecker.hs b/src/LambdaCube/SystemF/TypeChecker.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemF/TypeChecker.hs
@@ -0,0 +1,40 @@
+module LambdaCube.SystemF.TypeChecker where
+
+import           Data.List              (uncons)
+import           LambdaCube.SystemF.Ast
+
+substituteType :: Int -> LCType -> LCTerm -> LCTerm
+substituteType n v = go n
+  where
+    go _ e@(LCVar _)  = e
+    go m (LCLam t b)  = LCLam (substituteTypeInType m v t) $ go m b
+    go m (LCApp f a)  = go m f `LCApp` go m a
+    go m (LCTLam b)   = LCTLam $ go (m + 1) b
+    go m (LCTApp f t) = go m f `LCTApp` substituteTypeInType m v t
+
+substituteTypeInType :: Int -> LCType -> LCType -> LCType
+substituteTypeInType n v = go n
+  where
+    go _ LCBase       = LCBase
+    go m e@(LCTVar l) = if m == l then v else e
+    go m (LCArr a b)  = go m a `LCArr` go m b
+    go m (LCUniv a)   = LCUniv $ go (m + 1) a
+
+infer :: LCTerm -> Maybe LCType
+infer = go []
+  where
+    go tl (LCVar n) = fmap fst . uncons $ drop n tl
+    go tl (LCLam t b) = LCArr t <$> go (t : tl) b
+    go tl (LCApp f a)
+      | Just (LCArr at' rt) <- go tl f
+      , Just at <- go tl a
+      , at == at'
+      = Just rt
+      | otherwise
+      = Nothing
+    go tl (LCTLam b) = LCUniv <$> go tl b
+    go tl (LCTApp f t)
+      | Just (LCUniv rt) <- go tl f
+      = Just $ substituteTypeInType 0 t rt
+      | otherwise
+      = Nothing
diff --git a/src/LambdaCube/SystemFw/Ast.hs b/src/LambdaCube/SystemFw/Ast.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw/Ast.hs
@@ -0,0 +1,71 @@
+module LambdaCube.SystemFw.Ast where
+
+import           Data.Text                  (Text)
+import           Language.Haskell.TH.Syntax (Lift)
+
+data ExtLCType
+  = ExtLCBase
+  | ExtLCTVar Text
+  | ExtLCArr ExtLCType ExtLCType
+  | ExtLCUniv Text LCKind ExtLCType
+  | ExtLCTTLam Text LCKind ExtLCType
+  | ExtLCTTApp ExtLCType ExtLCType
+  deriving stock (Eq, Show, Lift)
+infixr 5 `ExtLCArr`
+infixl 6 `ExtLCTTApp`
+
+data ExtLCTerm
+  = ExtLCVar Text
+  | ExtLCLam Text ExtLCType ExtLCTerm
+  | ExtLCApp ExtLCTerm ExtLCTerm
+  | ExtLCTLam Text LCKind ExtLCTerm
+  | ExtLCTApp ExtLCTerm ExtLCType
+  deriving stock (Eq, Show, Lift)
+infixl 6 `ExtLCApp`
+infixl 6 `ExtLCTApp`
+
+data LCKind
+  = LCStar
+  | LCKArr LCKind LCKind
+  deriving stock (Eq, Show, Lift)
+infixr 5 `LCKArr`
+
+data LCType
+  = LCBase
+  | LCTVar Int
+  | LCArr LCType LCType
+  | LCUniv LCKind LCType
+  | LCTTLam LCKind LCType
+  | LCTTApp LCType LCType
+  deriving stock (Eq, Show, Lift)
+infixr 5 `LCArr`
+infixl 6 `LCTTApp`
+
+data LCTerm
+  = LCVar Int
+  | LCLam LCType LCTerm
+  | LCApp LCTerm LCTerm
+  | LCTLam LCKind LCTerm
+  | LCTApp LCTerm LCType
+  deriving stock (Eq, Show, Lift)
+infixl 6 `LCApp`
+infixl 6 `LCTApp`
+
+data LCValue
+  = LCValLam LCType LCTerm
+  | LCValTLam LCKind LCTerm
+  deriving stock (Eq, Show, Lift)
+
+data LCNormalTerm
+  = LCNormLam LCType LCNormalTerm
+  | LCNormTLam LCKind LCNormalTerm
+  | LCNormNeut LCNeutralTerm
+  deriving stock (Eq, Show, Lift)
+
+data LCNeutralTerm
+  = LCNeutVar Int
+  | LCNeutApp LCNeutralTerm LCNormalTerm
+  | LCNeutTApp LCNeutralTerm LCType
+  deriving stock (Eq, Show, Lift)
+infixl 6 `LCNeutApp`
+infixl 6 `LCNeutTApp`
diff --git a/src/LambdaCube/SystemFw/Elaborator.hs b/src/LambdaCube/SystemFw/Elaborator.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw/Elaborator.hs
@@ -0,0 +1,33 @@
+module LambdaCube.SystemFw.Elaborator where
+
+import           Data.List               (elemIndex)
+import           Data.Text               (Text)
+import qualified Data.Text               as Text
+import           LambdaCube.SystemFw.Ast
+
+elaborate :: ExtLCTerm -> Either String LCTerm
+elaborate = go [] []
+  where
+    go _  vl (ExtLCVar x)
+      | Just n <- x `elemIndex` vl
+      = Right $ LCVar n
+      | otherwise
+      = Left $ "Term variable " <> Text.unpack x <> " is not in scope"
+    go tl vl (ExtLCLam x t b) = LCLam <$> typeElaborate tl t <*> go tl (x : vl) b
+    go tl vl (ExtLCApp f a) = LCApp <$> go tl vl f <*> go tl vl a
+    go tl vl (ExtLCTLam x k b) = LCTLam k <$> go (x : tl) vl b
+    go tl vl (ExtLCTApp f t) = LCTApp <$> go tl vl f <*> typeElaborate tl t
+
+typeElaborate :: [Text] -> ExtLCType -> Either String LCType
+typeElaborate = go
+  where
+    go _ ExtLCBase = Right LCBase
+    go l (ExtLCTVar x)
+      | Just n <- x `elemIndex` l
+      = Right $ LCTVar n
+      | otherwise
+      = Left  $ "Type variable " <> Text.unpack x <> " is not in scope"
+    go l (ExtLCArr a b) = LCArr <$> go l a <*> go l b
+    go l (ExtLCUniv x k a) = LCUniv k <$> go (x : l) a
+    go l (ExtLCTTLam x k b) = LCTTLam k <$> go (x : l) b
+    go l (ExtLCTTApp f a) = LCTTApp <$> go l f <*> go l a
diff --git a/src/LambdaCube/SystemFw/Evaluator.hs b/src/LambdaCube/SystemFw/Evaluator.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw/Evaluator.hs
@@ -0,0 +1,35 @@
+module LambdaCube.SystemFw.Evaluator where
+
+import           LambdaCube.SystemFw.Ast
+import           LambdaCube.SystemFw.TypeChecker (substituteType)
+
+liftLCValue :: LCValue -> LCTerm
+liftLCValue (LCValLam t b)  = LCLam t b
+liftLCValue (LCValTLam k b) = LCTLam k b
+
+substitute :: Int -> LCValue -> LCTerm -> LCTerm
+substitute n v = go n
+  where
+    go m e@(LCVar l)  = if m == l then liftLCValue v else e
+    go m (LCLam t b)  = LCLam t $ go (m + 1) b
+    go m (LCApp f a)  = go m f `LCApp` go m a
+    go m (LCTLam k b) = LCTLam k $ go m b
+    go m (LCTApp f t) = go m f `LCTApp` t
+
+evaluate :: LCTerm -> LCValue
+evaluate = go
+  where
+    go (LCVar _) = error "Did you really type check this?"
+    go (LCLam t b) = LCValLam t b
+    go (LCApp f a)
+      | LCValLam _ b <- go f
+      , v <- go a
+      = go $ substitute 0 v b
+      | otherwise
+      = error "Did you really type check this?"
+    go (LCTLam k b) = LCValTLam k b
+    go (LCTApp f t)
+      | LCValTLam _ b <- go f
+      = go $ substituteType 0 t b
+      | otherwise
+      = error "Did you really type check this?"
diff --git a/src/LambdaCube/SystemFw/Normalizer.hs b/src/LambdaCube/SystemFw/Normalizer.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw/Normalizer.hs
@@ -0,0 +1,75 @@
+module LambdaCube.SystemFw.Normalizer where
+
+import           LambdaCube.SystemFw.Ast
+import           LambdaCube.SystemFw.TypeChecker (substituteTypeInType)
+
+substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
+substituteNormal n v = go n
+  where
+    go m (LCNormLam t b)  = LCNormLam t $ go (m + 1) b
+    go m (LCNormTLam k b) = LCNormTLam k $ go m b
+    go m (LCNormNeut nt)  = substituteNeutral m v nt
+
+substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
+substituteNeutral n v = go n
+  where
+    go m e@(LCNeutVar l)
+      | m == l = v
+      | otherwise = LCNormNeut e
+    go m (LCNeutApp f a) =
+      case go m f of
+        LCNormLam _ b  -> substituteNormal 0 a' b
+        LCNormTLam _ _ -> error "Did you really type check this?"
+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'
+      where
+        a' = substituteNormal m v a
+    go m (LCNeutTApp f t) =
+      case go m f of
+        LCNormLam _ _  -> error "Did you really type check this?"
+        LCNormTLam _ b -> substituteTypeNormal 0 t b
+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t
+
+substituteTypeNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm
+substituteTypeNormal n v = go n
+  where
+    go m (LCNormLam t b)  = LCNormLam (substituteTypeInType m v t) $ go m b
+    go m (LCNormTLam k b) = LCNormTLam k $ go (m + 1) b
+    go m (LCNormNeut nt)  = substituteTypeNeutral m v nt
+
+substituteTypeNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm
+substituteTypeNeutral n v = go n
+  where
+    go _ e@(LCNeutVar _) = LCNormNeut e
+    go m (LCNeutApp f a) =
+      case go m f of
+        LCNormLam _ b  -> substituteNormal 0 a' b
+        LCNormTLam _ _ -> error "Did you really type check this?"
+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'
+      where
+        a' = substituteTypeNormal m v a
+    go m (LCNeutTApp f t) =
+      case go m f of
+        LCNormLam _ _  -> error "Did you really type check this?"
+        LCNormTLam _ b -> substituteTypeNormal 0 t' b
+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t'
+      where
+        t' = substituteTypeInType m v t
+
+normalize :: LCTerm -> LCNormalTerm
+normalize = go
+  where
+    go (LCVar n) = LCNormNeut $ LCNeutVar n
+    go (LCLam t b) = LCNormLam t $ go b
+    go (LCTLam k b) = LCNormTLam k $ go b
+    go (LCApp f a) =
+      case go f of
+        LCNormLam _ b   -> substituteNormal 0 a' b
+        LCNormTLam _ _  -> error "Did you really type check this?"
+        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
+      where
+        a' = go a
+    go (LCTApp f t) =
+      case go f of
+        LCNormLam _ _   -> error "Did you really type check this?"
+        LCNormTLam _ b  -> substituteTypeNormal 0 t b
+        LCNormNeut neut -> LCNormNeut $ neut `LCNeutTApp` t
diff --git a/src/LambdaCube/SystemFw/Parser.hs b/src/LambdaCube/SystemFw/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw/Parser.hs
@@ -0,0 +1,74 @@
+module LambdaCube.SystemFw.Parser where
+
+import           Data.Foldable            (Foldable (foldl'))
+import           Data.Function            ((&))
+import           Data.Functor             (($>))
+import           Data.Maybe               (isJust)
+import           LambdaCube.Common.Parser
+import           LambdaCube.SystemFw.Ast
+import           Text.Megaparsec
+
+pTopLC :: Parser ExtLCTerm
+pTopLC = topParser pLC
+
+pLC :: Parser ExtLCTerm
+pLC = pTLam <|> pLam <|> pApp
+
+pTLam :: Parser ExtLCTerm
+pTLam =
+  ExtLCTLam
+  <$> (atsignBackslash *> identifier)
+  <*> (colon *> pKind)
+  <*> (dot *> pLC)
+
+pLam :: Parser ExtLCTerm
+pLam =
+  ExtLCLam
+  <$> (backslash *> identifier)
+  <*> (colon *> pType)
+  <*> (dot *> pLC)
+
+pApp :: Parser ExtLCTerm
+pApp = foldl' (&) <$> pATerm <*> many pAppArg
+
+pAppArg :: Parser (ExtLCTerm -> ExtLCTerm)
+pAppArg = do
+  isType <- isJust <$> optional atsign
+  if isType
+    then flip ExtLCTApp <$> pAType
+    else flip ExtLCApp <$> pATerm
+
+pATerm :: Parser ExtLCTerm
+pATerm = (ExtLCVar <$> identifier) <|> parenthesized pLC
+
+pType :: Parser ExtLCType
+pType = pTTLam <|> pUniv <|> pArr
+
+pTTLam :: Parser ExtLCType
+pTTLam =
+  ExtLCTTLam
+  <$> (backslash *> identifier)
+  <*> (colon *> pKind)
+  <*> (dot *> pType)
+
+pUniv :: Parser ExtLCType
+pUniv =
+  ExtLCUniv
+  <$> (exclamationMark *> identifier)
+  <*> (colon *> pKind)
+  <*> (comma *> pType)
+
+pArr :: Parser ExtLCType
+pArr = foldr1 ExtLCArr <$> sepBy1 pTTApp rightArrow
+
+pTTApp :: Parser ExtLCType
+pTTApp = foldl' ExtLCTTApp <$> pAType <*> many pAType
+
+pAType :: Parser ExtLCType
+pAType = (sharp $> ExtLCBase) <|> (ExtLCTVar <$> identifier) <|> parenthesized pType
+
+pKind :: Parser LCKind
+pKind = foldr1 LCKArr <$> sepBy1 pAKind rightArrow
+
+pAKind :: Parser LCKind
+pAKind = (asterisk $> LCStar) <|> parenthesized pKind
diff --git a/src/LambdaCube/SystemFw/PrettyPrinter.hs b/src/LambdaCube/SystemFw/PrettyPrinter.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw/PrettyPrinter.hs
@@ -0,0 +1,49 @@
+{- |
+  TODO: Use real pretty printer library
+-}
+{-# LANGUAGE OverloadedStrings #-}
+module LambdaCube.SystemFw.PrettyPrinter where
+
+import           Data.Text                       (Text)
+import qualified Data.Text                       as Text
+import           LambdaCube.Common.PrettyPrinter
+import           LambdaCube.SystemFw.Ast
+
+prettyKind :: LCKind -> Text
+prettyKind = prettyKindPrec 0
+
+prettyType :: LCType -> Text
+prettyType = prettyTypePrec 0
+
+prettyTerm :: LCTerm -> Text
+prettyTerm = prettyTermPrec 0
+
+prettyKindPrec :: Int -> LCKind -> Text
+prettyKindPrec = go
+  where
+    go _ LCStar       = "*"
+    go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
+
+prettyTypePrec :: Int -> LCType -> Text
+prettyTypePrec = go
+  where
+    pKP = prettyKindPrec
+
+    go _ LCBase        = "#"
+    go _ (LCTVar i)    = Text.pack $ show i
+    go p (LCArr a b)   = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
+    go p (LCUniv k b)  = wrapIfSpaced (p > 0) ["! :", pKP 0 k, ",", go 0 b]
+    go p (LCTTLam k b) = wrapIfSpaced (p > 0) ["\\ :", pKP 0 k, ".", go 0 b]
+    go p (LCTTApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
+
+prettyTermPrec :: Int -> LCTerm -> Text
+prettyTermPrec = go
+  where
+    pKP = prettyKindPrec
+    pTP = prettyTypePrec
+
+    go _ (LCVar i)    = Text.pack $ show i
+    go p (LCLam t b)  = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
+    go p (LCApp f a)  = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
+    go p (LCTLam k b) = wrapIfSpaced (p > 0) ["@\\ :", pKP 0 k, ".", go 0 b]
+    go p (LCTApp f t) = wrapIfSpaced (p > 1) [go 1 f, "@" <> pTP 1 t]
diff --git a/src/LambdaCube/SystemFw/TH.hs b/src/LambdaCube/SystemFw/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw/TH.hs
@@ -0,0 +1,44 @@
+module LambdaCube.SystemFw.TH where
+
+import           Control.Monad                  ((<=<))
+import qualified Data.Text                      as Text
+import           LambdaCube.SystemFw.Ast
+import           LambdaCube.SystemFw.Elaborator
+import           LambdaCube.SystemFw.Parser
+import           Language.Haskell.TH.Quote      (QuasiQuoter (..))
+import           Language.Haskell.TH.Syntax     (Loc (loc_start), Q, lift,
+                                                 location)
+import qualified Text.Megaparsec                as P
+import qualified Text.Megaparsec.Error          as PE
+
+systemFw :: QuasiQuoter
+systemFw =
+  QuasiQuoter
+    { quoteExp = lift <=< systemFwQuoteExp
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+systemFwQuoteExp :: String -> Q ExtLCTerm
+systemFwQuoteExp str = do
+  l <- location
+  case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
+    Right e  -> pure e
+    Left err -> fail $ PE.errorBundlePretty err
+
+elaboratedSystemFw :: QuasiQuoter
+elaboratedSystemFw =
+  QuasiQuoter
+    { quoteExp = lift <=< elaboratedSystemFwQuoteExp
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+elaboratedSystemFwQuoteExp :: String -> Q LCTerm
+elaboratedSystemFwQuoteExp str = do
+  e <- systemFwQuoteExp str
+  case elaborate e of
+    Right e' -> pure e'
+    Left err -> fail err
diff --git a/src/LambdaCube/SystemFw/TypeChecker.hs b/src/LambdaCube/SystemFw/TypeChecker.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw/TypeChecker.hs
@@ -0,0 +1,86 @@
+module LambdaCube.SystemFw.TypeChecker where
+
+import           Data.List               (uncons)
+import           LambdaCube.SystemFw.Ast
+
+substituteType :: Int -> LCType -> LCTerm -> LCTerm
+substituteType n v = go n
+  where
+    go _ e@(LCVar _)  = e
+    go m (LCLam t b)  = LCLam (substituteTypeInType m v t) $ go m b
+    go m (LCApp f a)  = go m f `LCApp` go m a
+    go m (LCTLam k b) = LCTLam k $ go (m + 1) b
+    go m (LCTApp f t) = go m f `LCTApp` substituteTypeInType m v t
+
+substituteTypeInType :: Int -> LCType -> LCType -> LCType
+substituteTypeInType n v = go n
+  where
+    go _ LCBase        = LCBase
+    go m e@(LCTVar l)  = if m == l then v else e
+    go m (LCArr a b)   = go m a `LCArr` go m b
+    go m (LCUniv k a)  = LCUniv k $ go (m + 1) a
+    go m (LCTTLam k b) = LCTTLam k $ go (m + 1) b
+    go m (LCTTApp f a) = go m f `LCTTApp` go m a
+
+reduceType :: LCType -> LCType
+reduceType = go
+  where
+    go LCBase = LCBase
+    go e@(LCTVar _) = e
+    go (LCArr a b) = go a `LCArr` go b
+    go (LCUniv k a) = LCUniv k $ go a
+    go (LCTTLam k b) = LCTTLam k $ go b
+    go (LCTTApp f a)
+      | LCTTLam _ b <- go f
+      , v <- go a
+      = go $ substituteTypeInType 0 v b
+      | otherwise
+      = error "Did you really kind check this?"
+
+infer :: LCTerm -> Maybe LCType
+infer = go []
+  where
+    go tl (LCVar n) = fmap fst . uncons $ drop n tl
+    go tl (LCLam t b)
+      | Just LCStar <- inferKind t
+      = LCArr v <$> go (v : tl) b
+      | otherwise
+      = Nothing
+      where
+        v = reduceType t
+    go tl (LCApp f a)
+      | Just (LCArr at' rt) <- go tl f
+      , Just at <- go tl a
+      , at == at'
+      = Just rt
+      | otherwise
+      = Nothing
+    go tl (LCTLam k b) = LCUniv k <$> go tl b
+    go tl (LCTApp f t)
+      | Just (LCUniv tk' rt) <- go tl f
+      , Just tk <- inferKind t
+      , tk == tk'
+      = Just $ substituteTypeInType 0 t rt
+      | otherwise
+      = Nothing
+
+inferKind :: LCType -> Maybe LCKind
+inferKind = go []
+  where
+    go _  LCBase = Just LCStar
+    go kl (LCTVar n) = fmap fst . uncons $ drop n kl
+    go kl (LCArr a b)
+      | Just LCStar <- go kl a
+      , Just LCStar <- go kl b
+      = Just LCStar
+      | otherwise
+      = Nothing
+    go kl (LCUniv k a) = go (k : kl) a
+    go kl (LCTTLam k b) = LCKArr k <$> go (k : kl) b
+    go kl (LCTTApp f a)
+      | Just (LCKArr ak' rk) <- go kl f
+      , Just ak <- go kl a
+      , ak == ak'
+      = Just rk
+      | otherwise
+      = Nothing
diff --git a/src/LambdaCube/SystemFw_/Ast.hs b/src/LambdaCube/SystemFw_/Ast.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw_/Ast.hs
@@ -0,0 +1,59 @@
+module LambdaCube.SystemFw_.Ast where
+
+import           Data.Text                  (Text)
+import           Language.Haskell.TH.Syntax (Lift)
+
+data ExtLCType
+  = ExtLCBase
+  | ExtLCTVar Text
+  | ExtLCArr ExtLCType ExtLCType
+  | ExtLCTTLam Text LCKind ExtLCType
+  | ExtLCTTApp ExtLCType ExtLCType
+  deriving stock (Eq, Show, Lift)
+infixr 5 `ExtLCArr`
+infixl 6 `ExtLCTTApp`
+
+data ExtLCTerm
+  = ExtLCVar Text
+  | ExtLCLam Text ExtLCType ExtLCTerm
+  | ExtLCApp ExtLCTerm ExtLCTerm
+  deriving stock (Eq, Show, Lift)
+infixl 6 `ExtLCApp`
+
+data LCKind
+  = LCStar
+  | LCKArr LCKind LCKind
+  deriving stock (Eq, Show, Lift)
+infixr 5 `LCKArr`
+
+data LCType
+  = LCBase
+  | LCTVar Int
+  | LCArr LCType LCType
+  | LCTTLam LCKind LCType
+  | LCTTApp LCType LCType
+  deriving stock (Eq, Show, Lift)
+infixr 5 `LCArr`
+infixl 6 `LCTTApp`
+
+data LCTerm
+  = LCVar Int
+  | LCLam LCType LCTerm
+  | LCApp LCTerm LCTerm
+  deriving stock (Eq, Show, Lift)
+infixl 6 `LCApp`
+
+data LCValue
+  = LCValLam LCType LCTerm
+  deriving stock (Eq, Show, Lift)
+
+data LCNormalTerm
+  = LCNormLam LCType LCNormalTerm
+  | LCNormNeut LCNeutralTerm
+  deriving stock (Eq, Show, Lift)
+
+data LCNeutralTerm
+  = LCNeutVar Int
+  | LCNeutApp LCNeutralTerm LCNormalTerm
+  deriving stock (Eq, Show, Lift)
+infixl 6 `LCNeutApp`
diff --git a/src/LambdaCube/SystemFw_/Elaborator.hs b/src/LambdaCube/SystemFw_/Elaborator.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw_/Elaborator.hs
@@ -0,0 +1,29 @@
+module LambdaCube.SystemFw_.Elaborator where
+
+import           Data.List                (elemIndex)
+import qualified Data.Text                as Text
+import           LambdaCube.SystemFw_.Ast
+
+elaborate :: ExtLCTerm -> Either String LCTerm
+elaborate = go []
+  where
+    go l (ExtLCVar x)
+      | Just n <- x `elemIndex` l
+      = Right $ LCVar n
+      | otherwise
+      = Left $ "Term variable " <> Text.unpack x <> " is not in scope"
+    go l (ExtLCLam x t b) = LCLam <$> typeElaborate t <*> go (x : l) b
+    go l (ExtLCApp f a) = LCApp <$> go l f <*> go l a
+
+typeElaborate :: ExtLCType -> Either String LCType
+typeElaborate = go []
+  where
+    go _ ExtLCBase = Right LCBase
+    go l (ExtLCTVar x)
+      | Just n <- x `elemIndex` l
+      = Right $ LCTVar n
+      | otherwise
+      = Left  $ "Type variable " <> Text.unpack x <> " is not in scope"
+    go l (ExtLCArr a b) = LCArr <$> go l a <*> go l b
+    go l (ExtLCTTLam x k b) = LCTTLam k <$> go (x : l) b
+    go l (ExtLCTTApp f a) = LCTTApp <$> go l f <*> go l a
diff --git a/src/LambdaCube/SystemFw_/Evaluator.hs b/src/LambdaCube/SystemFw_/Evaluator.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw_/Evaluator.hs
@@ -0,0 +1,25 @@
+module LambdaCube.SystemFw_.Evaluator where
+
+import           LambdaCube.SystemFw_.Ast
+
+liftLCValue :: LCValue -> LCTerm
+liftLCValue (LCValLam t b) = LCLam t b
+
+substitute :: Int -> LCValue -> LCTerm -> LCTerm
+substitute n v = go n
+  where
+    go m e@(LCVar l) = if m == l then liftLCValue v else e
+    go m (LCLam t b) = LCLam t (substitute (m + 1) v b)
+    go m (LCApp f a) = LCApp (go m f) (go m a)
+
+evaluate :: LCTerm -> LCValue
+evaluate = go
+  where
+    go (LCVar _) = error "Did you really type check this?"
+    go (LCLam t b) = LCValLam t b
+    go (LCApp f a)
+      | LCValLam _ b <- go f
+      , v <- go a
+      = go (substitute 0 v b)
+      | otherwise
+      = error "Did you really type check this?"
diff --git a/src/LambdaCube/SystemFw_/Normalizer.hs b/src/LambdaCube/SystemFw_/Normalizer.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw_/Normalizer.hs
@@ -0,0 +1,33 @@
+module LambdaCube.SystemFw_.Normalizer where
+
+import           LambdaCube.SystemFw_.Ast
+import           LambdaCube.SystemFw_.TypeChecker (reduceType)
+
+substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
+substituteNormal n v = go n
+  where
+    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b
+    go m (LCNormNeut nt) = substituteNeutral m v nt
+
+substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
+substituteNeutral n v = go n
+  where
+    go m e@(LCNeutVar l) = if m == l then v else LCNormNeut e
+    go m (LCNeutApp f a) =
+      case go m f of
+        LCNormLam _ b -> substituteNormal 0 a' b
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
+      where
+        a' = substituteNormal m v a
+
+normalize :: LCTerm -> LCNormalTerm
+normalize = go
+  where
+    go (LCVar n) = LCNormNeut $ LCNeutVar n
+    go (LCLam t b) = LCNormLam (reduceType t) $ go b
+    go (LCApp f a) =
+      case go f of
+        LCNormLam _ b   -> substituteNormal 0 a' b
+        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
+      where
+        a' = go a
diff --git a/src/LambdaCube/SystemFw_/Parser.hs b/src/LambdaCube/SystemFw_/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw_/Parser.hs
@@ -0,0 +1,51 @@
+module LambdaCube.SystemFw_.Parser where
+
+import           Data.Foldable            (Foldable (foldl'))
+import           Data.Functor             (($>))
+import           LambdaCube.Common.Parser
+import           LambdaCube.SystemFw_.Ast
+import           Text.Megaparsec
+
+pTopLC :: Parser ExtLCTerm
+pTopLC = topParser pLC
+
+pLC :: Parser ExtLCTerm
+pLC = pLam <|> pApp
+
+pLam :: Parser ExtLCTerm
+pLam =
+  ExtLCLam
+  <$> (backslash *> identifier)
+  <*> (colon *> pType)
+  <*> (dot *> pLC)
+
+pApp :: Parser ExtLCTerm
+pApp = foldl' ExtLCApp <$> pATerm <*> many pATerm
+
+pATerm :: Parser ExtLCTerm
+pATerm = (ExtLCVar <$> identifier) <|> parenthesized pLC
+
+pType :: Parser ExtLCType
+pType = pTTLam <|> pArr
+
+pTTLam :: Parser ExtLCType
+pTTLam =
+  ExtLCTTLam
+  <$> (backslash *> identifier)
+  <*> (colon *> pKind)
+  <*> (dot *> pType)
+
+pArr :: Parser ExtLCType
+pArr = foldr1 ExtLCArr <$> sepBy1 pTTApp rightArrow
+
+pTTApp :: Parser ExtLCType
+pTTApp = foldl' ExtLCTTApp <$> pAType <*> many pAType
+
+pAType :: Parser ExtLCType
+pAType = (sharp $> ExtLCBase) <|> (ExtLCTVar <$> identifier) <|> parenthesized pType
+
+pKind :: Parser LCKind
+pKind = foldr1 LCKArr <$> sepBy1 pAKind rightArrow
+
+pAKind :: Parser LCKind
+pAKind = (asterisk $> LCStar) <|> parenthesized pKind
diff --git a/src/LambdaCube/SystemFw_/PrettyPrinter.hs b/src/LambdaCube/SystemFw_/PrettyPrinter.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw_/PrettyPrinter.hs
@@ -0,0 +1,45 @@
+{- |
+  TODO: Use real pretty printer library
+-}
+{-# LANGUAGE OverloadedStrings #-}
+module LambdaCube.SystemFw_.PrettyPrinter where
+
+import           Data.Text                       (Text)
+import qualified Data.Text                       as Text
+import           LambdaCube.Common.PrettyPrinter
+import           LambdaCube.SystemFw_.Ast
+
+prettyKind :: LCKind -> Text
+prettyKind = prettyKindPrec 0
+
+prettyType :: LCType -> Text
+prettyType = prettyTypePrec 0
+
+prettyTerm :: LCTerm -> Text
+prettyTerm = prettyTermPrec 0
+
+prettyKindPrec :: Int -> LCKind -> Text
+prettyKindPrec = go
+  where
+    go _ LCStar       = "*"
+    go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
+
+prettyTypePrec :: Int -> LCType -> Text
+prettyTypePrec = go
+  where
+    pKP = prettyKindPrec
+
+    go _ LCBase        = "#"
+    go _ (LCTVar i)    = Text.pack $ show i
+    go p (LCArr a b)   = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
+    go p (LCTTLam k b) = wrapIfSpaced (p > 0) ["\\ :", pKP 0 k, ".", go 0 b]
+    go p (LCTTApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
+
+prettyTermPrec :: Int -> LCTerm -> Text
+prettyTermPrec = go
+  where
+    pTP = prettyTypePrec
+
+    go _ (LCVar i)   = Text.pack $ show i
+    go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
+    go p (LCApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
diff --git a/src/LambdaCube/SystemFw_/TH.hs b/src/LambdaCube/SystemFw_/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw_/TH.hs
@@ -0,0 +1,44 @@
+module LambdaCube.SystemFw_.TH where
+
+import           Control.Monad                   ((<=<))
+import qualified Data.Text                       as Text
+import           LambdaCube.SystemFw_.Ast
+import           LambdaCube.SystemFw_.Elaborator
+import           LambdaCube.SystemFw_.Parser
+import           Language.Haskell.TH.Quote       (QuasiQuoter (..))
+import           Language.Haskell.TH.Syntax      (Loc (loc_start), Q, lift,
+                                                  location)
+import qualified Text.Megaparsec                 as P
+import qualified Text.Megaparsec.Error           as PE
+
+systemFw_ :: QuasiQuoter
+systemFw_ =
+  QuasiQuoter
+    { quoteExp = lift <=< systemFw_QuoteExp
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+systemFw_QuoteExp :: String -> Q ExtLCTerm
+systemFw_QuoteExp str = do
+  l <- location
+  case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
+    Right e  -> pure e
+    Left err -> fail $ PE.errorBundlePretty err
+
+elaboratedSystemFw_ :: QuasiQuoter
+elaboratedSystemFw_ =
+  QuasiQuoter
+    { quoteExp = lift <=< elaboratedSystemFw_QuoteExp
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+elaboratedSystemFw_QuoteExp :: String -> Q LCTerm
+elaboratedSystemFw_QuoteExp str = do
+  e <- systemFw_QuoteExp str
+  case elaborate e of
+    Right e' -> pure e'
+    Left err -> fail err
diff --git a/src/LambdaCube/SystemFw_/TypeChecker.hs b/src/LambdaCube/SystemFw_/TypeChecker.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw_/TypeChecker.hs
@@ -0,0 +1,66 @@
+module LambdaCube.SystemFw_.TypeChecker where
+
+import           Data.List                (uncons)
+import           LambdaCube.SystemFw_.Ast
+
+substituteTypeInType :: Int -> LCType -> LCType -> LCType
+substituteTypeInType n v = go n
+  where
+    go _ LCBase        = LCBase
+    go m e@(LCTVar l)  = if m == l then v else e
+    go m (LCArr a b)   = go m a `LCArr` go m b
+    go m (LCTTLam k b) = LCTTLam k $ go (m + 1) b
+    go m (LCTTApp f a) = go m f `LCTTApp` go m a
+
+reduceType :: LCType -> LCType
+reduceType = go
+  where
+    go LCBase = LCBase
+    go e@(LCTVar _) = e
+    go (LCArr a b) = go a `LCArr` go b
+    go (LCTTLam k b) =  LCTTLam k $ go b
+    go (LCTTApp f a)
+      | LCTTLam _ b <- go f
+      , v <- go a
+      = go $ substituteTypeInType 0 v b
+      | otherwise
+      = error "Did you really kind check this?"
+
+infer :: LCTerm -> Maybe LCType
+infer = go []
+  where
+    go tl (LCVar n) = fmap fst . uncons $ drop n tl
+    go tl (LCLam t b)
+      | Just LCStar <- inferKind t
+      = LCArr v <$> go (v : tl) b
+      | otherwise
+      = Nothing
+      where
+        v = reduceType t
+    go tl (LCApp f a)
+      | Just (LCArr at' rt) <- go tl f
+      , Just at <- go tl a
+      , at == at'
+      = Just rt
+      | otherwise
+      = Nothing
+
+inferKind :: LCType -> Maybe LCKind
+inferKind = go []
+  where
+    go _  LCBase = Just LCStar
+    go kl (LCTVar n) = fmap fst . uncons $ drop n kl
+    go kl (LCArr a b)
+      | Just LCStar <- go kl a
+      , Just LCStar <- go kl b
+      = Just LCStar
+      | otherwise
+      = Nothing
+    go kl (LCTTLam k b) = LCKArr k <$> go (k : kl) b
+    go kl (LCTTApp f a)
+      | Just (LCKArr ak' rk) <- go kl f
+      , Just ak <- go kl a
+      , ak == ak'
+      = Just rk
+      | otherwise
+      = Nothing
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}