diff --git a/changelog.md b/changelog.md
new file mode 100644
index 0000000..ce1351a
--- /dev/null
+++ b/changelog.md
@@ -0,0 +1,21 @@
+# 0.3.0 - WIP
+- `String` literals
+- Exponentiation operation on floats (and their `Descriptor` analysis)
+- Scientific notation accepted for floating-point literals
+- `None` type (and its constructor `None`) built-in.
+- `sqrt` function that is well-typed.
+- Gradable booleans and conditional expressions
+- `Species` and `Basis` descriptors 
+- Python-style `def` function blocks with typed arguments and `return`
+
+# 0.2.0 - PROPL 2026 announcement (June 15, 2026)
+- Pythonic syntax in types
+- Typing now includes implicit types with type dependency (for resolving Float which has kind `{d : Descriptor} -> d -> Type`
+- REPL `fortli`
+
+# 0.1.0 - Initial version
+
+- Straight line numerical code (with lambdas), Pythonic style.
+- Type checking (with annotations).
+Floats are graded abelian groups, graded by Descriptors which are generated by the free-abelian group over constructors names (which do not need defining and can be arbitrarily introduced, but must be guarded by Unit and Quantity constructors). 
+- Combinator for composing `Descriptor` values: `& : Descriptor -> Descriptor -> Descriptor` which behaves a bit like linear logic 'with' (additive conjunction).
\ No newline at end of file
diff --git a/examples/coriolis.frtl.output b/examples/coriolis.frtl.output
new file mode 100644
index 0000000..4af1832
--- /dev/null
+++ b/examples/coriolis.frtl.output
@@ -0,0 +1 @@
+None
\ No newline at end of file
diff --git a/examples/diffusion.frtl.output b/examples/diffusion.frtl.output
new file mode 100644
index 0000000..4af1832
--- /dev/null
+++ b/examples/diffusion.frtl.output
@@ -0,0 +1 @@
+None
\ No newline at end of file
diff --git a/examples/flow-rate.frtl b/examples/flow-rate.frtl
index 3828cc6..99eb0b9 100644
--- a/examples/flow-rate.frtl
+++ b/examples/flow-rate.frtl
@@ -1,16 +1,23 @@
 ## Small-orifice flow problem (Torricelli's law)
+def small_orifice_flow(area, h):
+  """Area of the orifice"""
+  area : Float[Unit[m^2]]
 
-# Area of the orifice
-area : Float[Unit[m^2]] = 0.0
+  """Distance from water surface to orifice"""
+  h : Float[Unit[m]]
 
-# Acceleration of gravity
-gravity : Float[Unit[m / s^2]] = 9.8065
+  """Acceleration of gravity"""
+  gravity : Float[Unit[m / s^2]] = 9.8065
 
-#  Distance from water surface to orifice
-h : Float[Unit[m]] = 0.0
+  """Ratio of actual flow to ideal flow"""
+  discharge_coefficient : Float[Unit[1]] = 0.61
 
-# Ratio of actual flow to ideal flow
-discharge_coefficient : Float[Unit[1]] = 0.61
+  q : Float[Unit[m ^ 3 / s]] = (discharge_coefficient
+    * area * sqrt((2.0 : Float[Unit[1]]) * gravity * h))
 
-q : Float[Unit[m ^ 3 / s]] = (discharge_coefficient
-                               * area * sqrt((2.0 : Float[Unit[1]]) * gravity * h))
\ No newline at end of file
+  return q
+
+# Example
+area : Float[Unit[m^2]] = 10.0
+h    : Float[Unit[m]]   = 5.0
+it = small_orifice_flow(area, h)
\ No newline at end of file
diff --git a/examples/flow-rate.frtl.output b/examples/flow-rate.frtl.output
new file mode 100644
index 0000000..6d5a64b
--- /dev/null
+++ b/examples/flow-rate.frtl.output
@@ -0,0 +1 @@
+60.406948
\ No newline at end of file
diff --git a/src/Lang/Desugar.hs b/src/Lang/Desugar.hs
index afc4920..fb6db64 100644
--- a/src/Lang/Desugar.hs
+++ b/src/Lang/Desugar.hs
@@ -3,20 +3,31 @@
 
 module Lang.Desugar where
 
+-- Lowers a program into a desugared state (for simpler interpreter)
+
 import Lang.Syntax
+import Lang.TypeError
 
 import Control.Monad.Trans.State
-import Control.Monad.Trans.Writer
 import Control.Monad.Trans.Class     (lift)
 
 import Data.Foldable                 (traverse_)
+import qualified Data.Map.Lazy as Map
 
-newtype ST = ST { next_var :: Integer }
+-- Desugarer state
+data ST = ST
+    { next_var :: Integer
+      -- Stack of type annotations that have been found inline
+    , pendingAnnotations :: [Map.Map Identifier (Type 0)]
+      -- Stack of desugared defs, one list per nested function body being desugared
+    , outputDefs :: [[Def 'Desugared]]
+    }
 
 initState :: ST
-initState = ST 0
+initState = ST 0 [Map.empty] [[]]
 
-type Desugar = StateT ST (Writer [Def 'Desugared])
+-- Desugarer monad
+type Desugar = StateT ST (Either TypeError)
 
 freshVar :: Desugar Identifier
 freshVar = do
@@ -25,22 +36,76 @@ freshVar = do
     put $ st { next_var = i + 1 }
     return $ "_" ++ show i
 
-desugar :: Program 'Parsed -> Program 'Desugared
-desugar p = 
-    let m = traverse_ desugarDef p
-        (_, out) = runWriter (runStateT m initState)
-    in out
+-- Convert from a parsed program to a desugared one
+desugar :: Program 'Parsed -> Either TypeError (Program 'Desugared)
+desugar p = head . outputDefs <$> execStateT (traverse_ desugarDef p) initState
 
--- | Add desugared definitions to the output of the desugaring pass.
+-- | Add desugared definitions to the top of the output stack.
 emitDefs :: [Def 'Desugared] -> Desugar ()
-emitDefs = lift . tell
+emitDefs defs = modify $ \st -> st { outputDefs = (head (outputDefs st) ++ defs) : tail (outputDefs st) }
 
 desugarDef :: Def 'Parsed -> Desugar ()
 desugarDef (TypeDef id ty1 ty2) = emitDefs [TypeDef id ty1 ty2]
 desugarDef (DataDef id cs ty)   = emitDefs [DataDef id cs ty]
 desugarDef (ImportDef spec)     = emitDefs [ImportDef spec]
 desugarDef (Return e)           = emitDefs [Return e]
-desugarDef (ValDef lhs e)       = do desugarVal lhs e
+
+desugarDef (AnnDef id ty) =
+  -- Add the typing annotation of id (into the head stack)
+  modify $ \st -> st { pendingAnnotations = 
+                            Map.insert id ty (head $ pendingAnnotations st)
+                            : (tail $ pendingAnnotations st) }
+
+desugarDef (FunDef id args body) = do
+  -- Push a new annotation map and defs list onto their stacks
+  modify $ \st -> st { pendingAnnotations = Map.empty : pendingAnnotations st
+                     , outputDefs = [] : outputDefs st }
+  -- Desugar the body
+  traverse_ desugarDef body
+  -- Pop the body's desugared defs and annotations off their stacks
+  st <- get
+  let body' = head (outputDefs st)
+      headAnnotations = head (pendingAnnotations st)
+  put (st { outputDefs = tail (outputDefs st), pendingAnnotations = tail (pendingAnnotations st) })
+  -- Resolve the types into the parameters
+  typedParams <- lift $ resolveFunctionParameterTypes args headAnnotations
+  emitDefs [FunDefElaborated id typedParams body']
+
+desugarDef (ValDef lhs e) = do
+    lhs' <- applyPendingAnnotation lhs
+    desugarVal lhs' e
+
+-- | Resolve the declared types of a function's parameters before lowering its
+-- body to a lambda expression. Parameters can come with their type or have
+-- their type given as a standalon annotation in the body
+-- There should be exactly one of these, not both
+resolveFunctionParameterTypes :: [(Identifier, Maybe (Type 0))] -> Map.Map Identifier (Type 0) -> Either TypeError [(Identifier, Type 0)]
+resolveFunctionParameterTypes args annotations = mapM fillIn args
+    where
+      fillIn (param_var, Nothing) = 
+        case Map.lookup param_var annotations of
+          Nothing -> Left $ WellFormednessError $ MissingParameterAnnotation param_var
+          Just ty -> Right (param_var, ty)
+      fillIn (param_var, Just ty) =
+        case Map.lookup param_var annotations of
+          Nothing  -> Right (param_var, ty)
+          Just ty' -> Left $ WellFormednessError $ DuplicateParameterAnnotation param_var
+
+applyPendingAnnotation :: Lhs 'Parsed -> Desugar (Lhs 'Parsed)
+applyPendingAnnotation lhs = do
+    st <- get
+    let (lhs', annotations) = applyAnnotation (head $ pendingAnnotations st) lhs
+    put $ st { pendingAnnotations = annotations : (tail $ pendingAnnotations st) }
+    return lhs'
+
+-- | Apply and consume a preceding standalone annotation when the binding has
+-- no inline annotation. Inline annotations remain authoritative.
+applyAnnotation :: Map.Map Identifier (Type 0) -> Lhs 'Parsed -> (Lhs 'Parsed, Map.Map Identifier (Type 0))
+applyAnnotation annotations lhs@(VarLhs id Nothing) =
+    case Map.lookup id annotations of
+        Just ty -> (VarLhs id (Just ty), Map.delete id annotations)
+        Nothing -> (lhs, annotations)
+applyAnnotation annotations lhs = (lhs, annotations)
 
 -- (a, (b1, b2)) = c
 -- _0 = c
diff --git a/src/Lang/Frontend.hs b/src/Lang/Frontend.hs
index 38901bb..d59c98e 100644
--- a/src/Lang/Frontend.hs
+++ b/src/Lang/Frontend.hs
@@ -5,7 +5,7 @@ module Lang.Frontend where
 import Lang.Options
 import Lang.Parser      (parseProgram)
 import Lang.PrettyPrint (pprint)
-import Lang.Semantics   (interpret, Env)
+import Lang.Semantics   (interpret, Env, Value)
 import Lang.Desugar     (desugar)
 import Lang.Syntax
 import Lang.Types
@@ -36,7 +36,7 @@ main = do
           putStrLn $ pprint result
           exitSuccess
 
-run :: Bool -> String -> IO (Either String (Program 'Parsed, [Option], Env, Expr, Context))
+run :: Bool -> String -> IO (Either String (Program 'Parsed, [Option], Env, Value, Context))
 run report fname = do
   -- Check if this is a file
   exists <- doesPathExist fname
@@ -50,21 +50,27 @@ run report fname = do
       input <- readFile fname
       case parseProgram fname input of
         Right (parsetree, options) -> do
-          let ast = desugar parsetree
-          -- Evaluate
-          let (env, normalForm) = interpret options ast
-          -- Typing
-          case typeInference options ast of
-              Left err -> do
-                let ?srcFile = fname
-                putStrLn $ ansi_bold <> ansi_red
-                        <> "Not well-typed.\n" <> errorToString err <> ansi_reset
-                return $ Left (errorToString err)
-              Right (ctxt, ty) -> do
-                putStrLn $ ansi_bold <> ansi_green
-                        <> "Well-typed " <> ansi_reset
-                        <> ansi_bold <> "as " <> ansi_reset <> pprint ty
-                return $ Right (parsetree, options, env, normalForm, ctxt)
+          case desugar parsetree of
+            Left err -> do
+              let ?srcFile = fname
+              putStrLn $ ansi_bold <> ansi_red
+                      <> "Not well-formed.\n" <> errorToString err <> ansi_reset
+              return $ Left (errorToString err)
+            Right ast -> do
+              -- Evaluate
+              let (env, normalForm) = interpret options ast
+              -- Typing
+              case typeInference options ast of
+                Left err -> do
+                  let ?srcFile = fname
+                  putStrLn $ ansi_bold <> ansi_red
+                    <> "Not well-typed.\n" <> errorToString err <> ansi_reset
+                  return $ Left (errorToString err)
+                Right (ctxt, ty) -> do
+                  putStrLn $ ansi_bold <> ansi_green
+                    <> "Well-typed " <> ansi_reset
+                    <> ansi_bold <> "as " <> ansi_reset <> pprint ty
+                  return $ Right (parsetree, options, env, normalForm, ctxt)
         Left msg -> do
           putStrLn $ ansi_red ++ "Error: " ++ ansi_reset ++ msg
           return $ Left msg
diff --git a/src/Lang/Kinding.hs b/src/Lang/Kinding.hs
index 1ddfadb..cc4b3f6 100644
--- a/src/Lang/Kinding.hs
+++ b/src/Lang/Kinding.hs
@@ -17,10 +17,10 @@ import Lang.TypeHelpers
 -- Check if a type is well-kinded against the second argument (kind)
 -- and if so, elaborate any implicit arguments in the type
 checkKind :: Type 0 -> Type 1 -> Either TypeError (Type 0)
-checkKind (FunTy t1 t2) k = do
-  t1' <- checkKind t1 k
+checkKind (FunTy ts t2) k = do
+  ts' <- mapM (`checkKind` k) ts
   t2' <- checkKind t2 k
-  return $ FunTy t1' t2'
+  return $ FunTy ts' t2'
 
 -- e.g. Float[U[m]]
 -- :k Float : {d : Desc} -> d -> Type
@@ -29,7 +29,7 @@ checkKind (FunTy t1 t2) k = do
 checkKind t@(TyApp t1 t2) k = do
   (t1', k1) <- synthKind t1
   case k1 of
-    FunTy k1' k2 ->
+    FunTy [k1'] k2 ->
         case kindEquality k2 (IsSpec k) of
           Left err -> Left err
           Right () -> do
@@ -37,7 +37,7 @@ checkKind t@(TyApp t1 t2) k = do
                return $ TyApp t1' t2'
     -- Since ImplictTys must come with an ImplicitTyApp
     -- then this means we have an implicit application here
-    ImplicitFunTy var k1' (FunTy (TyVar var') k3) | var == var' -> do
+    ImplicitFunTy var k1' (FunTy [TyVar var'] k3) | var == var' -> do
       -- We therefore have to synth the kind of t2
       (t2', k2) <- synthKind t2
       -- this is now what we want to specialise k1' at
@@ -83,15 +83,15 @@ checkKind t k = do
 
 
 checkSort :: Type 1 -> Type 2 -> Either TypeError (Type 1)
-checkSort (FunTy t1 t2) k = do
-  t1' <- checkSort t1 k
+checkSort (FunTy ts t2) k = do
+  ts' <- mapM (`checkSort` k) ts
   t2' <- checkSort t2 k
-  return $ FunTy t1' t2'
+  return $ FunTy ts' t2'
 
 checkSort t@(TyApp t1 t2) k = do
   (t1', k1) <- synthSort t1
   case k1 of
-    FunTy k1' k2 ->
+    FunTy [k1'] k2 ->
         if k == k2
             then do
                t2' <- checkSort t2 k1'
@@ -117,15 +117,15 @@ synthSort (TyCon (SuccP (SuccP _)) c) =
 synthSort (TyApp t1 t2) = do
   (t1', k) <- synthSort t1
   case k of
-    FunTy k1 k2 -> do
+    FunTy [k1] k2 -> do
         t2' <- checkSort t2 k1
         return (TyApp t1' t2', k2)
     _ -> Left $ ExpectingFunctionSort k
 
-synthSort (FunTy t1 t2) = do
-  (t1', k) <- synthSort t1
+synthSort (FunTy ts t2) = do
+  (ts', k) <- synthSortFunctionArguments ts
   t2'      <- checkSort t2 k
-  return (FunTy t1' t2', k)
+  return (FunTy ts' t2', k)
 
 synthSort (ImplicitFunTy var t1 t2) = do
   -- TODO: need synthOrder?
@@ -159,11 +159,11 @@ synthKind t@(TyCon ZeroP c) =
 synthKind (TyApp t1 t2) = do
   (t1', k) <- synthKind t1
   case k of
-    FunTy k1 k2 -> do
+    FunTy [k1] k2 -> do
         t2' <- checkKind t2 k1
         return (TyApp t1' t2', k2)
 
-    ImplicitFunTy var k1' (FunTy (TyVar var') k3) | var == var' -> do
+    ImplicitFunTy var k1' (FunTy [TyVar var'] k3) | var == var' -> do
       -- We therefore have to synth the kind of t2
       (t2', k2) <- synthKind t2
       -- this is now what we want to specialise k1' at
@@ -181,10 +181,10 @@ synthKind (ImplicitTyApp t1 t2) = do
     _ -> Left $ ExpectingFunctionKind k
 
 
-synthKind (FunTy t1 t2) = do
-  (t1', k) <- synthKind t1
+synthKind (FunTy ts t2) = do
+  (ts', k) <- synthKindFunctionArguments ts
   t2'      <- checkKind t2 k
-  return (FunTy t1' t2', k)
+  return (FunTy ts' t2', k)
 
 synthKind (ProdTy t1 t2) = do
   (t1', t2', k) <- synthCheckPair t1 t2
@@ -228,6 +228,20 @@ synthCheckPair t1 t2 =
       t2' <- checkKind t2 k
       return (t1', t2', k)
 
+synthKindFunctionArguments :: [Type 0] -> Either TypeError ([Type 0], Type 1)
+synthKindFunctionArguments [] = Left $ ContextualError "Function types must have at least one argument"
+synthKindFunctionArguments (t:ts) = do
+  (t', k) <- synthKind t
+  ts' <- mapM (`checkKind` k) ts
+  return (t' : ts', k)
+
+synthSortFunctionArguments :: [Type 1] -> Either TypeError ([Type 1], Type 2)
+synthSortFunctionArguments [] = Left $ ContextualError "Function kinds must have at least one argument"
+synthSortFunctionArguments (t:ts) = do
+  (t', k) <- synthSort t
+  ts' <- mapM (`checkSort` k) ts
+  return (t' : ts', k)
+
 indent :: String -> String
 indent = unlines . map ("  " <>) . lines
 
diff --git a/src/Lang/Lexer.x b/src/Lang/Lexer.x
index 39434c3..7e640c2 100755
--- a/src/Lang/Lexer.x
+++ b/src/Lang/Lexer.x
@@ -20,6 +20,7 @@ $alpha  = [a-zA-Z\_\-]
 $lower  = [a-z]
 $upper  = [A-Z]
 $eol    = [\n]
+$hwhite = [\ \t]
 $alphanum  = [$alpha $digit \_]
 @sym    = ($lower | $upper) ($alphanum | \')*
 @tyvar    = \' @sym
@@ -32,15 +33,16 @@ $alphanum  = [$alpha $digit \_]
 
 tokens :-
 
-  $white*$eol                   { \p s -> TokenNL p }
+  $hwhite*$eol                  { \p s -> TokenNL p }
   $eol+                         { \p s -> TokenNL p }
-  $white+                       ;
+  $hwhite+                      ;
   "#" .*                        ;
   @tyvar                          { \p s -> TokenTyVar p (tail s) }
   lang\.@langPrag               { \p s -> TokenLang p s }
   forall                        { \p _ -> TokenForall p }
   data                          { \p s -> TokenData p }
   let                           { \p s -> TokenLet p }
+  def                           { \p s -> TokenDef p }
   in                            { \p s -> TokenIn p }
   succ                          { \p s -> TokenSucc p }
   zero                          { \p s -> TokenZero p }
@@ -89,6 +91,7 @@ tokens :-
 data Token
   = TokenLang     AlexPosn String
   | TokenData     AlexPosn
+  | TokenDef      AlexPosn
   | TokenCase     AlexPosn
   | TokenSep      AlexPosn
   | TokenLet      AlexPosn
@@ -106,6 +109,8 @@ data Token
   | TokenLParen   AlexPosn
   | TokenRParen   AlexPosn
   | TokenNL       AlexPosn
+  | TokenIndent   AlexPosn
+  | TokenDedent   AlexPosn
   | TokenSig      AlexPosn
   | TokenEquiv    AlexPosn
   | TokenHole     AlexPosn
@@ -149,7 +154,61 @@ tyVarString :: Token -> String
 tyVarString (TokenTyVar _ x) = x
 tyVarString t = error $ "Not a type variable " ++ show t
 
-scanTokens = alexScanTokens . stripDocstrings >>= (return . trim)
+scanTokens = alexScanTokens . stripDocstrings >>= (return . trim . layout)
+
+-- Add layout markers for function bodies. Existing multiline expressions use
+-- indentation for readability, so layout is activated only after a def header.
+-- A stack of block columns supports arbitrarily nested defs.
+layout :: [Token] -> [Token]
+layout tokens = go [] tokens [] 0
+  where
+    -- go <tokens of current line so far> <remaining tokens> <block column stack> <paren depth>
+    go _ [] stack _ = map (const (TokenDedent (AlexPn 0 0 0))) stack
+    go line (t:ts) stack parenDepth =
+      case t of
+        TokenNL p ->
+          let (next, _) = nextNonNL ts
+              lineHeader = isDefHeader line
+              nextColumn = maybe 0 (snd . getPos) next
+              newline = if (not (null stack) && parenDepth == 0)
+                           || lineHeader || lineStartsImport line
+                        then [t]
+                        else []
+              (popped, remaining) = span (> nextColumn) stack
+              (emitted, stack')
+                -- indentation is ignored inside parentheses
+                | parenDepth /= 0 = (newline, stack)
+                -- block opens after a def header: nl before indent
+                | lineHeader && nextColumn > lineColumn line =
+                    (newline ++ [TokenIndent p], nextColumn : stack)
+                -- blocks close: one dedent per level, before the nl so the
+                -- enclosing block still sees a statement separator
+                | otherwise =
+                    (map (const (TokenDedent p)) popped ++ newline, remaining)
+          in emitted ++ go [] ts stack' parenDepth
+        _ -> t : go (line ++ [t]) ts stack (parenDepth + parenthesisDepth t)
+
+    nextNonNL [] = (Nothing, [])
+    nextNonNL (TokenNL _ : ts) = nextNonNL ts
+    nextNonNL (t:ts) = (Just t, ts)
+
+    lineColumn [] = 0
+    lineColumn (t:_) = snd (getPos t)
+
+    isDefHeader line = any isDef line && any isColon line
+    isDef (TokenDef _) = True
+    isDef _ = False
+    isColon (TokenSig _) = True
+    isColon _ = False
+
+    parenthesisDepth (TokenLParen _) = 1
+    parenthesisDepth (TokenRParen _) = -1
+    parenthesisDepth _ = 0
+
+    lineStartsImport (TokenLang _ _ : _) = True
+    lineStartsImport (TokenImport _ : _) = True
+    lineStartsImport (TokenFrom _ : _) = True
+    lineStartsImport _ = False
 
 -- Strip Python-style triple-quoted docstrings before lexing.
 -- We preserve newlines to keep parser layout/error positions stable.
diff --git a/src/Lang/Parser.y b/src/Lang/Parser.y
index df5cd77..cfec29a 100644
--- a/src/Lang/Parser.y
+++ b/src/Lang/Parser.y
@@ -25,6 +25,9 @@ import Lang.Options
 %token
     nl      { TokenNL _ }
     data    { TokenData _ }
+    def     { TokenDef _ }
+    indent  { TokenIndent _ }
+    dedent  { TokenDedent _ }
     from    { TokenFrom _ }
     import  { TokenImport _ }
     cast    { TokenCast _ }
@@ -109,6 +112,7 @@ ImportList :: { [Identifier] }
 
 Defs :: { [Option] -> Program 'Parsed }
   : Def NL Defs           { \opts -> ($1 opts) : ($3 opts) }
+  | Def Defs              { \opts -> ($1 opts) : ($2 opts) }
   | return Expr           { \opts -> [Return ($2 opts)] }
   | Def                   { \opts -> [$1 opts] }
 
@@ -118,13 +122,31 @@ NL :: { () }
 
 Def :: { [Option] -> Def 'Parsed}
   : Lhs '=' Expr          { \opts -> ValDef ($1 opts) ($3 opts) }
+  | IDENT ':' Type        { \opts -> AnnDef (symString $1) ($3 opts) }
+  | def IDENT '(' Parameters ')' ':' nl indent BlockDefs dedent
+                           { \opts -> FunDef (symString $2) ($4 opts) ($9 opts) }
 --  | data IDENT ':' Kind '=' ConstructorList { \opts -> DataDef (symString $2) ($6 opts) ($4 opts) }
 
+Parameters :: { [Option] -> [(Identifier, Maybe (Type 0))] }
+  : IDENT ':' Type ',' Parameters
+                           { \opts -> (symString $1, Just ($3 opts)) : ($5 opts) }
+  | IDENT ':' Type         { \opts -> [(symString $1, Just ($3 opts))] }
+  | IDENT ',' Parameters   { \opts -> (symString $1, Nothing) : ($3 opts) }
+  | IDENT                  { \_ -> [(symString $1, Nothing)] }
+  | {- empty -}            { \_ -> [] }
+
+BlockDefs :: { [Option] -> [Def 'Parsed] }
+  : nl BlockDefs           { $2 }
+  | Def nl BlockDefs       { \opts -> ($1 opts) : ($3 opts) }
+  | return Expr nl         { \opts -> [Return ($2 opts)] }
+  | Def                    { \opts -> [$1 opts] }
+  | return Expr            { \opts -> [Return ($2 opts)] }
+
 Lhs :: { [Option] -> Lhs 'Parsed }
-  : IDENT { \opts -> VarLhs (symString $1) Nothing }
-  | IDENT ':' Type { \opts -> VarLhs (symString $1) (Just $ $3 opts) }
-  | Lhs ',' Lhs { \opts -> PairLhs ($1 opts) ($3 opts) }
-  | '(' Lhs ')' { $2 }
+  : IDENT                  { \opts -> VarLhs (symString $1) Nothing }
+  | IDENT ':' Type         { \opts -> VarLhs (symString $1) (Just ($3 opts)) }
+  | Lhs ',' Lhs            { \opts -> PairLhs ($1 opts) ($3 opts) }
+  | '(' Lhs ')'            { $2 }
 
 ConstructorList :: { [Option] -> [(Identifier, [Type 0])] }
 ConstructorList
@@ -134,10 +156,9 @@ ConstructorList
 
 Expr :: { [Option] -> Expr }
   : let IDENT '=' Expr in Expr
-    { \opts ->
-      MkGenLet (mkPos $1) (symString $2) ($4 opts) ($6 opts) }
+    { \opts -> MkLet (mkPos $1) (symString $2) ($4 opts) ($6 opts) }
 
-   -- TODO: probably needs reconciling with lambda syntax
+  -- TODO: probably needs reconciling with lambda syntax
   | Lam IDENT '->' Expr
     { \opts -> MkTyAbs (mkPos $1) (symString $2) ($4 opts) }
 
@@ -179,13 +200,14 @@ Form :: { [Option] -> Expr }
 
 Kind :: { [Option] -> Type 1 }
 Kind
-  : Kind '->' Kind   { \opts -> FunTy ($1 opts) ($3 opts) }
+  : Kind '->' Kind   { \opts -> FunTy [$1 opts] ($3 opts) }
   | IDENT            { \opts -> case symString $1 of
                                   k -> tyCon1 k }
-  
+
 Type :: { [Option] -> Type 0 }
 Type
-  : Type '->' Type        { \opts -> FunTy ($1 opts) ($3 opts) }
+  : ManyTypes '->' Type        { \opts -> FunTy ($1 opts) ($3 opts) }
+  | '(' ')'   '->' Type        { \opts -> FunTy [] ($4 opts) }
   | Type '*' Type         { \opts -> ProdTy ($1 opts) ($3 opts) }
   | Type '+' Type         { \opts -> SumTy ($1 opts) ($3 opts) }
   | Type '&' Type         { \opts -> WithTy ($1 opts) ($3 opts) }
@@ -196,6 +218,16 @@ Type
   | TypeAtom              { \opts -> $1 opts }
   | forall IDENT '.' Type { \opts -> Forall (symString $2) ($4 opts) }
 
+ManyTypes :: { [Option] -> [Type 0] }
+ManyTypes
+  : '(' ManyTypesMore ')' { \opts -> $2 opts }
+  | Type                  { \opts -> [$1 opts] }
+
+ManyTypesMore :: { [Option] -> [Type 0] }
+ManyTypesMore
+  : Type ',' ManyTypesMore  { \opts -> ($1 opts) : ($3 opts) }
+  | Type                    { \opts -> [$1 opts] }
+
 NumFloat :: { Float }
 NumFloat
   : FLOAT { let (TokenFloat _ x) = $1 in read x }
@@ -203,25 +235,32 @@ NumFloat
 
 TypeAtom :: { [Option] -> Type 0 }
 TypeAtom
-  : IDENT            { \opts -> tyCon0 $ symString $1 }
+  : '(' ')'          { \_ -> tyCon0 "()" }
+  | IDENT            { \opts -> tyCon0 $ symString $1 }
   | TYVAR            { \opts -> TyVar $ tyVarString $1 }
   | '(' Type ')'     { \opts -> $2 opts }
   | INT              { \opts -> tyCon0 $ let (TokenInt _ x) = $1 in x }
   | '?'              { \opts -> tyCon0 "?" }
 
 Juxt :: { [Option] -> Expr }
-  : Juxt '(' Expr ')'                 { \opts -> App ($1 opts) ($3 opts) }
-  | Juxt '[' Type ']'                 { \opts -> App ($1 opts) (TyEmbed ($3 opts)) }
+  : Juxt '(' Arguments ')'            { \opts -> App ($1 opts) ($3 opts) }
+  | Juxt '(' ')'                      { \opts -> App ($1 opts) [] }
+  | Juxt '[' Type ']'                 { \opts -> App ($1 opts) [TyEmbed ($3 opts)] }
   | cast '(' Atom ')'                 { \opts -> MkCast (mkPos $1) ($3 opts) }
   | Atom                      { $1 }
 
+Arguments :: { [Option] -> [Expr] }
+  : Form ',' Arguments                { \opts -> ($1 opts) : ($3 opts) }
+  | Form                              { \opts -> [$1 opts] }
+
 Atom :: { [Option] -> Expr }
-  : '(' Expr ')'              { $2 }
+  : '(' ')'                   { \_ -> Con "()" [] }
+  | '(' Expr ')'              { $2 }
   | IDENT                     { \opts -> MkVar (mkPos $1) (symString $1) }
   | LAMBDA '(' IDENT ':' Type ')' ':' Expr
-    { \opts -> MkAbs (mkPos $1) (symString $3) (Just ($5 opts)) ($8 opts) }
+    { \opts -> MkAbs (mkPos $1) [(symString $3, Just ($5 opts))] ($8 opts) }
   | LAMBDA IDENT ':' Expr
-    { \opts -> MkAbs (mkPos $1) (symString $2) Nothing ($4 opts) }
+    { \opts -> MkAbs (mkPos $1) [(symString $2, Nothing)] ($4 opts) }
   | zero
     { \opts -> MkZero (mkPos $1) }
   | succ
diff --git a/src/Lang/PrettyPrint.hs b/src/Lang/PrettyPrint.hs
index 6f49f6b..c0520b2 100644
--- a/src/Lang/PrettyPrint.hs
+++ b/src/Lang/PrettyPrint.hs
@@ -5,6 +5,7 @@
 module Lang.PrettyPrint where
 
 import Lang.Syntax
+import Data.List (intercalate)
 
 -- Pretty print terms
 class PrettyPrint t where
@@ -25,14 +26,12 @@ instance PrettyPrint Expr where
     isLexicallyAtomic (NumInteger _) = True
     isLexicallyAtomic _       = False
 
-    pprint (Abs var Nothing e)  = "lambda " ++ var ++ ": " ++ pprint e
-    pprint (Abs var (Just t) e) = "lambda (" ++ var ++ " : " ++ pprint t ++ "): " ++ pprint e
-    pprint (App (Abs var mt e1) e2) =
-      bracket_pprint (Abs var mt e1) ++ " " ++ bracket_pprint e2
-    pprint (App (Sig e1 t) e2) =
-      bracket_pprint (Sig e1 t) ++ " " ++ bracket_pprint e2
-    pprint (App e1 (TyEmbed t)) = pprint e1 ++ "[" ++ pprint t ++ "]"
-    pprint (App e1 e2) = pprint e1 ++ " " ++ bracket_pprint e2
+    pprint (Abs params e) = "lambda " ++ intercalate ", " (map pprintParam params) ++ ": " ++ pprint e
+      where
+        pprintParam (x, Nothing) = x
+        pprintParam (x, Just t)  = "(" ++ x ++ " : " ++ pprint t ++ ")"
+    pprint (App e1 [TyEmbed t]) = pprint e1 ++ "[" ++ pprint t ++ "]"
+    pprint (App e1 es) = pprint e1 ++ "(" ++ intercalate ", " (map pprint es) ++ ")"
     pprint (Var var) = var
     pprint (Sig e t) = bracket_pprint e ++ " : " ++ pprint t
     pprint (Cast t)  = "cast " ++ pprint t
@@ -40,7 +39,7 @@ instance PrettyPrint Expr where
     pprint (TyAbs var e) = "/\\" ++ var ++ " -> " ++ pprint e
     pprint (TyEmbed t) = "[" ++ pprint t ++ "]"
     -- ML
-    pprint (GenLet x e1 e2) = "let " ++ x ++ " = " ++ pprint e1 ++ " in " ++ pprint e2
+    pprint (Let x e1 e2) = "let " ++ x ++ " = " ++ pprint e1 ++ " in " ++ pprint e2
     -- PCF expressions
     pprint Zero                   = "zero"
     pprint Succ                   = "succ"
@@ -101,8 +100,12 @@ instance PrettyPrint (Type i) where
     pprint (TyCon _ c) = c
     pprint (ImplicitFunTy var tyA tyB) =
       "{" ++ var ++ " : " ++ pprint tyA ++ "} -> " ++ pprint tyB
-    pprint (FunTy tyA tyB) =
+      
+    pprint (FunTy [tyA] tyB) =
       bracket_pprint tyA ++ " -> " ++ pprint tyB
+    pprint (FunTy tys tyB) =
+      "(" ++ intercalate ", " (map bracket_pprint tys) ++ ") -> " ++ pprint tyB
+
     pprint (ProdTy tyA tyB) =
       bracket_pprint tyA ++ " * " ++ bracket_pprint tyB
     pprint (SumTy tyA tyB) =
diff --git a/src/Lang/Primitives.hs b/src/Lang/Primitives.hs
index aa440e0..80e2ee2 100644
--- a/src/Lang/Primitives.hs
+++ b/src/Lang/Primitives.hs
@@ -36,6 +36,7 @@ desc2 = tyCon2 "Descriptor"
 dataConstructors :: [(Identifier, Type 0)]
 dataConstructors = [
     ("None"     , tyCon0 "None")
+  , ("()"       , tyCon0 "()")
   , ("True"     , boolTy (tyCon0 "1"))
   , ("False"    , boolTy (tyCon0 "1"))
  ]
@@ -43,18 +44,19 @@ dataConstructors = [
 typeConstructors :: [(Identifier, Type 1)]
 typeConstructors = [
      -- Graded float
-    ("Float"    , ImplicitFunTy "d" desc2 (FunTy (tyVar "d") type0))
+    ("Float"    , ImplicitFunTy "d" desc2 (FunTy [tyVar "d"] type0))
      -- Graded integer
-  , ("Integer"  , ImplicitFunTy "d" desc2 (FunTy (tyVar "d") type0))
+  , ("Integer"  , ImplicitFunTy "d" desc2 (FunTy [tyVar "d"] type0))
      -- Graded string
-  , ("String"  , ImplicitFunTy "d" desc2 (FunTy (tyVar "d") type0))
+  , ("String"  , ImplicitFunTy "d" desc2 (FunTy [tyVar "d"] type0))
     -- Graded boolean
-  , ("Bool"     , ImplicitFunTy "d" desc2 (FunTy (tyVar "d") type0))
+  , ("Bool"     , ImplicitFunTy "d" desc2 (FunTy [tyVar "d"] type0))
   , ("Nat"      , type0)
-  , ("Unit"     , FunTy type0 (tyCon1 "UoM"))
-  , ("Quantity" , FunTy type0 (tyCon1 "KoQ"))
-  , ("Species"  , FunTy type0 (tyCon1 "SpeciesType"))
-  , ("Basis"    , FunTy type0 (tyCon1 "BasisType"))
+  , ("()"       , type0)
+  , ("Unit"     , FunTy [type0] (tyCon1 "UoM"))
+  , ("Quantity" , FunTy [type0] (tyCon1 "KoQ"))
+  , ("Species"  , FunTy [type0] (tyCon1 "SpeciesType"))
+  , ("Basis"    , FunTy [type0] (tyCon1 "BasisType"))
   , ("m"        , type0)
   , ("s"        , type0)
   , ("None"     , type0)
@@ -79,7 +81,7 @@ kindConstructors = [
   , ("BasisType" , desc2)
   , ("Base"     , desc2) -- The base Descriptor (bottom)
   -- Products of descriptors
-  , ("&"        , FunTy desc2 (FunTy desc2 desc2))
+  , ("&"        , FunTy [desc2, desc2] desc2)
   ]
 
 
@@ -93,7 +95,7 @@ agroup = tyCon1 "AGroup"
 isDescConstructor :: Identifier -> Maybe (Type 1)
 isDescConstructor conId =
   case lookup conId typeConstructors of
-    Just k@(FunTy t _) | t == desc -> Just k
+    Just k@(FunTy [t] _) | t == desc -> Just k
     Just k@(ImplicitFunTy _ t _) | t == desc2 -> Just k
     _                              -> Nothing
 
diff --git a/src/Lang/REPL.hs b/src/Lang/REPL.hs
index 5626a12..225fa2a 100644
--- a/src/Lang/REPL.hs
+++ b/src/Lang/REPL.hs
@@ -7,7 +7,7 @@ import Lang.Frontend    (banner, run, ansi_bold, ansi_reset)
 import Lang.Parser      (parseExpr, parseType)
 import Lang.PrettyPrint (pprint)
 import Lang.Types       (synth, errorToString, Context)
-import Lang.Semantics   (bigStep, Env)
+import Lang.Semantics   (bigStep, Env, emptyEnv, Value)
 import Lang.Kinding     (synthKind)
 import Lang.Options     (Option)
 
@@ -35,7 +35,7 @@ initialState :: REPLState
 initialState = REPLState {
      currentFile = Nothing
    , prompt      = "[F]"
-   , env         = []
+   , env         = emptyEnv
    , options     = []
    , typingContext = []
   }
@@ -125,7 +125,7 @@ replLoop state = do
 trim :: String -> String
 trim = reverse . dropWhile isSpace . reverse
 
-displayResult :: Expr -> IO ()
+displayResult :: Value -> IO ()
 displayResult e = do
   putStrLn $ pprint e
 
diff --git a/src/Lang/Semantics.hs b/src/Lang/Semantics.hs
index 4f470d8..a057569 100644
--- a/src/Lang/Semantics.hs
+++ b/src/Lang/Semantics.hs
@@ -6,71 +6,168 @@ module Lang.Semantics where
 import Lang.Syntax
 import Lang.Options
 import Lang.Substitution
+import Lang.PrettyPrint
 import Lang.Primitives (dataConstructors)
+import qualified Data.Map.Lazy as Map
 -- import Debug.Trace
 
-type Env = [(Identifier, Expr)]
+-- **************************************
+-- ** Evaluation context and values
+-- ***************************************
+
+-- Result of evaluating is a value which is either a (normal form) expression
+-- or a function closure
+data Value =
+    VClosure   { closureParams :: [Identifier], closureBody :: [Def 'Desugared], closureEnv :: Env }
+  | VPrimitive { primitiveName :: String, primitiveFunc :: [Value] -> Either String Value }
+  | ValExpr Expr
+
+instance PrettyPrint Value where
+  pprint (ValExpr e) = pprint e
+  pprint (VPrimitive name _) = "<primitive:" ++ name ++ ">"
+  pprint (VClosure params _ _) = "<function/" ++ show (length params) ++ ">"
+
+-- | Project a normal-form expression out of a value
+-- (closures have no expression form)
+valueToExpr :: Value -> Either String Expr
+valueToExpr (ValExpr e) = Right e
+valueToExpr VClosure{}  = Left "Cannot use a function value here"
+valueToExpr VPrimitive{} = Left "Cannot use a primitive value here"
+
+-- Environment
+data Env = Env
+    { bindings :: Map.Map Identifier Value
+    , parent   :: Maybe Env
+    }
+
+primitives :: [(Identifier, Value)]
+primitives = [ ("sqrt", VPrimitive "sqrt" sqrtFunc)]
+  where
+    sqrtFunc [ValExpr (NumFloat n)] = Right $ ValExpr $ NumFloat $ sqrt n
+    sqrtFunc _ = Left "sqrt expects a single float argument" 
+
+-- Empty env (at top of lexical scope)
+emptyEnv :: Env
+emptyEnv = Env (Map.fromList primitives) Nothing
+
+-- Add binding in the current frame
+bindHere :: Identifier -> Value -> Env -> Env
+bindHere id val (Env bindings parent) =
+  Env (Map.insert id val bindings) parent
+
+lookupBinding :: Identifier -> Env -> Either String Value
+lookupBinding name env =
+  case Map.lookup name (bindings env) of
+    Just value -> Right value
+    Nothing ->
+      case parent env of
+        Just outer -> lookupBinding name outer
+        Nothing    -> Left $ "Unbound variable: " ++ name
+
+-- **************************************
+-- ** Interpreter for definitions
+-- ***************************************
 
 -- Evaluate a program to normal form
-interpret :: [Option] -> Program 'Desugared -> (Env, Expr)
-interpret = interpretDefs []
+interpret :: [Option] -> Program 'Desugared -> (Env, Value)
+interpret = interpretDefs emptyEnv
 
 -- Interpret the definitions, including building an environment
 -- for the rest of the program
-interpretDefs :: Env -> [Option] -> Program 'Desugared -> (Env, Expr)
+interpretDefs :: Env -> [Option] -> Program 'Desugared -> (Env, Value)
 
-interpretDefs env opts ((ValDef (VarLhs id _) e):defs) = 
+interpretDefs env opts ((ValDef (VarLhs id _) e):defs) =
   case bigStep env opts e of
-    Right v -> interpretDefs ((id, v) : env) opts defs
+    Right v -> interpretDefs (bindHere id v env) opts defs
     Left err -> error err
 
+interpretDefs env opts ((FunDefElaborated id params body):defs) =
+  -- Make a closure capturing the environment and proceed
+  let env' = bindHere id (VClosure (map fst params) body env) env
+  in interpretDefs env' opts defs
+
 -- Return expression
-interpretDefs env opts ((Return e):defs) = 
+interpretDefs env opts ((Return e):defs) =
   case bigStep env opts e of
     Right v -> (env, v)
     Left err -> error err
 
-interpretDefs env opts (_:defs ) = interpretDefs env opts defs
+-- TODO: work out what handling we need here
+interpretDefs env opts (TypeDef{}:defs)   = interpretDefs env opts defs
+interpretDefs env opts (DataDef{}:defs)   = interpretDefs env opts defs
+interpretDefs env opts (ImportDef{}:defs) = interpretDefs env opts defs
 
-interpretDefs env opts [] = 
+interpretDefs env opts [] =
   -- No definition
-  -- return the expression fro the last binder if there is one
-  case lookup "it" env of
-    Just v  -> (env, v)
-    Nothing -> (env, Con "None" [])
-
--- Big step operational model (i.e., expression interpreter)
-bigStep :: Env -> [Option] -> Expr -> Either String Expr
--- Special-cased primitive: sqrt
-bigStep env opts (App (Var "sqrt") e2) =
-  case bigStep env opts e2 of
-    Right (NumFloat n) -> return $ NumFloat $ sqrt n
-    Right _            -> Left "sqrt expects a number"
-    Left err           -> Left err
-bigStep env opts (App e1 e2) =
-  case bigStep env opts e1 of
-    Left err -> Left err
-    Right (Abs x _ body) ->
-      case bigStep env opts e2 of
-        Left err -> Left err
-        Right v2 -> bigStep env opts (substitute body (x, v2))
-    Right (TyAbs var body) ->
-      case bigStep env opts e2 of
-        Left err -> Left err
-        Right (TyEmbed t) -> bigStep env opts (substitute body (var, TyEmbed t))
-        Right _ -> Left "Type application expects a type"
-    Right _ -> Left "Application expects a function"
+  -- return the expression for the last binder if there is one
+  case lookupBinding "it" env of
+    Right v  -> (env, v)
+    Left _   -> (env, ValExpr (Con "None" []))
+
+-- **************************************
+-- ** Interpreter for expressions
+-- ***************************************
+
+bigStep :: Env -> [Option] -> Expr -> Either String Value
+
+bigStep env opts (App e1 es) = do
+  v1 <- bigStep env opts e1
+  apply v1 es
+  where
+    -- local loop: a Value cannot be wrapped back into an App node, and
+    -- over-application must re-apply the resulting value to the leftover args
+    apply (VClosure params body capturedEnv) es
+      -- full or partial (curried) application
+      | length es <= length params = do
+          let (paramsHere, paramsRest) = splitAt (length es) params
+          -- Evaluate the arguments
+          vs <- mapM (bigStep env opts) es
+          -- Make new environment for the closure, binding the parameters to the evaluated arguments
+          let env' = Env { bindings = Map.fromList (zip paramsHere vs), parent = Just capturedEnv }
+          if null paramsRest
+            then Right $ snd $ interpretDefs env' opts body
+            else Right $ VClosure paramsRest body env'
+
+      -- over-application: apply the arguments this closure takes, then apply
+      -- the resulting value to the rest
+      | otherwise = do
+          let (esHere, esRest) = splitAt (length params) es
+          vs <- mapM (bigStep env opts) esHere
+          let env' = Env { bindings = Map.fromList (zip params vs), parent = Just capturedEnv }
+          apply (snd (interpretDefs env' opts body)) esRest
+
+    apply (VPrimitive _ f) es = do
+      vs <- mapM (bigStep env opts) es
+      f vs
+
+    -- Type abstraction: uses a substitution (rather than environment) to avoid
+    -- having to carry around type environments
+    apply (ValExpr (TyAbs var body)) es =
+      case es of
+        [e2] -> do
+          v2 <- bigStep env opts e2
+          case v2 of
+            ValExpr (TyEmbed t) -> bigStep env opts (substitute body (var, TyEmbed t))
+            _ -> Left "Type application expects a type"
+        _ -> Left "Type application expects one type"
+
+    apply _ _ = Left "Application expects a function"
+
 bigStep env opts (Sig e _) = bigStep env opts e
 bigStep env opts (Cast e) = bigStep env opts e
-bigStep env opts (Var x) = case lookup x env of
-  Just v  -> Right v
-  Nothing ->
-    case lookup x dataConstructors of
-      Just _  -> Right (Con x [])
-      Nothing -> Left $ "Unbound variable: " ++ x
-bigStep env opts (GenLet x e1 e2) = do
+bigStep env opts (Var x) =
+  case lookupBinding x env of
+    Right v  -> Right v
+    Left _   ->
+      -- If the variable is not bound, check if it is a data constructor
+      -- If so, return the constructor with no arguments
+      case lookup x dataConstructors of
+        Just _  -> Right (ValExpr (Con x []))
+        Nothing -> Left $ "Unbound variable: " ++ x
+
+bigStep env opts (Let x e1 e2) = do
   v1 <- bigStep env opts e1
-  bigStep ((x, v1) : env) opts e2
+  bigStep (bindHere x v1 env) opts e2
 
 bigStep env opts (Case eg branchl branchr) = do
   error "Not implemented yet"
@@ -80,23 +177,27 @@ bigStep env opts (Case eg branchl branchr) = do
 --     Inr e2 -> bigStep ((fst branchr, e2) : env) opts (snd branchr)
 --     _      -> Left "case expects a sum type"
 
-bigStep env opts (Fst e) =
-  case bigStep env opts e of
-    Right (Pair e1 _) -> bigStep env opts e1
+bigStep env opts (Fst e) = do
+  v <- bigStep env opts e
+  case v of
+    -- pair components are already in normal form
+    ValExpr (Pair e1 _) -> Right $ ValExpr e1
     _         -> Left "fst expects a pair"
-bigStep env opts (Snd e) =
-  case bigStep env opts e of
-    Right (Pair _ e2) -> bigStep env opts e2
+bigStep env opts (Snd e) = do
+  v <- bigStep env opts e
+  case v of
+    ValExpr (Pair _ e2) -> Right $ ValExpr e2
     _         -> Left "snd expects a pair"
+
 bigStep env opts (Pair e1 e2) = do
-  v1 <- bigStep env opts e1
-  v2 <- bigStep env opts e2
-  return $ Pair v1 v2
+  v1 <- bigStep env opts e1 >>= valueToExpr
+  v2 <- bigStep env opts e2 >>= valueToExpr
+  return $ ValExpr $ Pair v1 v2
 bigStep env opts (Lift e _) = bigStep env opts e
 bigStep env opts (BinOp op e1 e2) = do
-  v1 <- bigStep env opts e1
-  v2 <- bigStep env opts e2
-  case (v1, v2) of
+  v1 <- bigStep env opts e1 >>= valueToExpr
+  v2 <- bigStep env opts e2 >>= valueToExpr
+  ValExpr <$> case (v1, v2) of
     (NumFloat n1, NumFloat n2) ->
       case op of
         BinOpExp    -> return $ NumFloat $ n1 ** n2
@@ -121,14 +222,14 @@ bigStep env opts (BinOp op e1 e2) = do
         BinOpOr     -> Left "Logical OR is not defined for integers"
     (Con b1 [], Con b2 []) ->
       case op of
-        BinOpAnd -> 
+        BinOpAnd ->
           case (b1, b2) of
             ("True", "True")   -> return $ Con "True" []
             ("True", "False")  -> return $ Con "False" []
             ("False", "True")  -> return $ Con "False" []
             ("False", "False") -> return $ Con "False" []
             _ -> Left "Logical AND operation expects two booleans"
-        BinOpOr  -> 
+        BinOpOr  ->
           case (b1, b2) of
             ("True", "True")   -> return $ Con "True" []
             ("True", "False")  -> return $ Con "True" []
@@ -138,8 +239,8 @@ bigStep env opts (BinOp op e1 e2) = do
         _ -> Left "Binary operation undefined for given inputs"
     _ -> Left "Error in binary operation evaluation"
 bigStep env opts (UnOp op e) = do
-  v <- bigStep env opts e
-  case v of
+  v <- bigStep env opts e >>= valueToExpr
+  ValExpr <$> case v of
     (NumFloat n) ->
       case op of
         UnOpNegate -> return $ NumFloat $ -n
@@ -150,7 +251,7 @@ bigStep env opts (UnOp op e) = do
         UnOpNot    -> Left "Logical NOT is not defined for integers"
     (Con b []) ->
       case op of
-        UnOpNot -> 
+        UnOpNot ->
           case b of
             "True" -> return $ Con "False" []
             "False" -> return $ Con "True" []
@@ -160,19 +261,20 @@ bigStep env opts (UnOp op e) = do
 bigStep env opts (Cond e1 e2 e3) = do
   v2 <- bigStep env opts e2
   case v2 of
-    Con "True" []  -> bigStep env opts e1
-    Con "False" [] -> bigStep env opts e3
+    ValExpr (Con "True" [])  -> bigStep env opts e1
+    ValExpr (Con "False" []) -> bigStep env opts e3
     _              -> Left "Condition expects a boolean"
 
 -- Values
-bigStep env opts (TyEmbed e) = Right $ TyEmbed e -- TODO: remove this
-bigStep env opts (TyAbs x e) = Right $ TyAbs x e
-bigStep env opts (NumFloat f) = Right $ NumFloat f
-bigStep env opts (NumInteger n) = Right $ NumInteger n
-bigStep env opts (StringConst s) = Right $ StringConst s
-bigStep env opts Succ = Right Succ
-bigStep env opts Zero = Right Zero
-bigStep env opts (Abs x mt body) = Right $ Abs x mt body
+bigStep env opts (TyEmbed e) = Right $ ValExpr $ TyEmbed e -- TODO: remove this
+bigStep env opts (TyAbs x e) = Right $ ValExpr $ TyAbs x e
+bigStep env opts (NumFloat f) = Right $ ValExpr $ NumFloat f
+bigStep env opts (NumInteger n) = Right $ ValExpr $ NumInteger n
+bigStep env opts (StringConst s) = Right $ ValExpr $ StringConst s
+bigStep env opts Succ = Right $ ValExpr Succ
+bigStep env opts Zero = Right $ ValExpr Zero
+-- A lambda closes over its environment; its body becomes a single-return block
+bigStep env opts (Abs params body) = Right $ VClosure (map fst params) [Return body] env
 bigStep env opts (Con c es) = do
-  vs <- mapM (bigStep env opts) es
-  return $ Con c vs
+  vs <- mapM (\e -> bigStep env opts e >>= valueToExpr) es
+  return $ ValExpr $ Con c vs
diff --git a/src/Lang/Substitution.hs b/src/Lang/Substitution.hs
index 0bb33a2..1e44045 100644
--- a/src/Lang/Substitution.hs
+++ b/src/Lang/Substitution.hs
@@ -21,18 +21,23 @@ substituteExpr (Var y) (x, e')
   | x == y = e'
   | otherwise = Var y
 
-substituteExpr (App e1 e2) s =
-  App (substituteExpr e1 s) (substituteExpr e2 s)
+substituteExpr (App e1 es) s =
+  App (substituteExpr e1 s) (map (`substituteExpr` s) es)
 
-substituteExpr (Abs y mt e) s =
-  let (y', e') = substitute_binding y e s in Abs y' mt e'
+substituteExpr (Abs [] e) s = Abs [] (substituteExpr e s)
+substituteExpr (Abs ((x, mt):params) e) s =
+  -- treat the remaining parameters as the body of a nested abstraction so
+  -- capture-avoidance can reuse the single-binder logic per parameter
+  case substitute_binding x (Abs params e) s of
+    (x', Abs params' e') -> Abs ((x', mt) : params') e'
+    _ -> error "substitute_binding on Abs must preserve Abs shape"
 
 substituteExpr (Sig e t) s = Sig (substituteExpr e s) t
 
 -- ML
 
-substituteExpr (GenLet x e1 e2) s =
-  let (x' , e2') = substitute_binding x e2 s in GenLet x' (substituteExpr e1 s) e2'
+substituteExpr (Let x e1 e2) s =
+  let (x' , e2') = substitute_binding x e2 s in Let x' (substituteExpr e1 s) e2'
 
 -- Casts
 substituteExpr (Cast e) s =
@@ -109,8 +114,8 @@ class SubstituteType l where
   substituteType :: Type l -> (Identifier, Type l) -> Type l
 
 instance SubstituteType 0 where
-  substituteType (FunTy t1 t2) s =
-    FunTy (substituteType t1 s) (substituteType t2 s)
+  substituteType (FunTy ts t2) s =
+    FunTy (map (`substituteType` s) ts) (substituteType t2 s)
 
   substituteType (TyCon p c) s = TyCon p c
 
@@ -146,8 +151,8 @@ instance SubstituteType 1 where
     let (var', t2') = substitute_binding var t2 s
     in ImplicitFunTy var' t1 t2'
 
-  substituteType (FunTy t1 t2) s =
-    FunTy (substituteType t1 s) (substituteType t2 s)
+  substituteType (FunTy ts t2) s =
+    FunTy (map (`substituteType` s) ts) (substituteType t2 s)
 
   substituteType (TyCon p c) s = TyCon p c
 
diff --git a/src/Lang/Syntax.hs b/src/Lang/Syntax.hs
index a51436a..2ed9309 100644
--- a/src/Lang/Syntax.hs
+++ b/src/Lang/Syntax.hs
@@ -31,6 +31,14 @@ data ImportSpec
 type Program (p :: Phase) = [Def p]
 
 data Def (p :: Phase) where
+    -- Parsed phase definitions
+    AnnDef  :: Identifier -> Type 0 -> Def 'Parsed
+    FunDef  :: Identifier -> [(Identifier, Maybe (Type 0))] -> [Def 'Parsed] -> Def 'Parsed
+    
+    -- Desugared phase definitions
+    FunDefElaborated  :: Identifier -> [(Identifier, Type 0)] -> [Def 'Desugared] -> Def 'Desugared
+    
+    -- Any phase definitions
     ValDef  :: Lhs p -> Expr -> Def p
     TypeDef :: Identifier -> Type n -> Type (1 + n) -> Def p
     DataDef :: Identifier -> [(Identifier, [Type n])] -> Type (1 + n) -> Def p -- Currently not implemented beyond front end
@@ -53,13 +61,13 @@ type HasPairLhsC p = (HasPairLhs p ~ 'True)
 -- and construction. Use the Mk* constructors directly when you need to supply or
 -- inspect source positions.
 data Expr where
-    MkAbs :: Maybe SrcPos -> Identifier -> Maybe (Type 0) -> Expr -> Expr
-    MkApp :: Maybe SrcPos -> Expr ->  Expr   -> Expr
+    MkAbs :: Maybe SrcPos -> [(Identifier, Maybe (Type 0))] -> Expr -> Expr
+    MkApp :: Maybe SrcPos -> Expr -> [Expr]  -> Expr
     MkVar :: Maybe SrcPos -> Identifier      -> Expr
     MkSig :: Maybe SrcPos -> Expr -> Type 0  -> Expr
     MkTyAbs   :: Maybe SrcPos -> Identifier -> Expr -> Expr
     MkTyEmbed :: Maybe SrcPos -> Type 0             -> Expr
-    MkGenLet :: Maybe SrcPos -> Identifier -> Expr -> Expr -> Expr
+    MkLet :: Maybe SrcPos -> Identifier -> Expr -> Expr -> Expr
     MkCast :: Maybe SrcPos -> Expr -> Expr
     MkZero :: Maybe SrcPos -> Expr
     MkSucc :: Maybe SrcPos -> Expr
@@ -79,13 +87,13 @@ data Expr where
 
 -- | Extract the source position from any Expr node
 exprPos :: Expr -> Maybe SrcPos
-exprPos (MkAbs p _ _ _)     = p
+exprPos (MkAbs p _ _)       = p
 exprPos (MkApp p _ _)       = p
 exprPos (MkVar p _)         = p
 exprPos (MkSig p _ _)       = p
 exprPos (MkTyAbs p _ _)     = p
 exprPos (MkTyEmbed p _)     = p
-exprPos (MkGenLet p _ _ _)  = p
+exprPos (MkLet p _ _ _)     = p
 exprPos (MkCast p _)        = p
 exprPos (MkZero p)          = p
 exprPos (MkSucc p)          = p
@@ -105,13 +113,13 @@ exprPos (MkCond p _ _ _)    = p
 -- | Position-agnostic pattern synonyms.
 -- In a pattern they match regardless of the stored position.
 -- As expressions they construct with Nothing as the position.
-pattern Abs :: Identifier -> Maybe (Type 0) -> Expr -> Expr
-pattern Abs x mt e <- MkAbs _ x mt e
-  where Abs x mt e = MkAbs Nothing x mt e
+pattern Abs :: [(Identifier, Maybe (Type 0))] -> Expr -> Expr
+pattern Abs params e <- MkAbs _ params e
+  where Abs params e = MkAbs Nothing params e
 
-pattern App :: Expr -> Expr -> Expr
-pattern App e1 e2 <- MkApp _ e1 e2
-  where App e1 e2 = MkApp Nothing e1 e2
+pattern App :: Expr -> [Expr] -> Expr
+pattern App e1 es <- MkApp _ e1 es
+  where App e1 es = MkApp Nothing e1 es
 
 pattern Var :: Identifier -> Expr
 pattern Var x <- MkVar _ x
@@ -129,9 +137,9 @@ pattern TyEmbed :: Type 0 -> Expr
 pattern TyEmbed t <- MkTyEmbed _ t
   where TyEmbed t = MkTyEmbed Nothing t
 
-pattern GenLet :: Identifier -> Expr -> Expr -> Expr
-pattern GenLet x e1 e2 <- MkGenLet _ x e1 e2
-  where GenLet x e1 e2 = MkGenLet Nothing x e1 e2
+pattern Let :: Identifier -> Expr -> Expr -> Expr
+pattern Let x e1 e2 <- MkLet _ x e1 e2
+  where Let x e1 e2 = MkLet Nothing x e1 e2
 
 pattern Cast :: Expr -> Expr
 pattern Cast e <- MkCast _ e
@@ -193,11 +201,11 @@ pattern Cond :: Expr -> Expr -> Expr -> Expr
 pattern Cond e1 e2 e3 <- MkCond _ e1 e2 e3
   where Cond e1 e2 e3 = MkCond Nothing e1 e2 e3
 
-{-# COMPLETE MkAbs, MkApp, MkVar, MkSig, MkTyAbs, MkTyEmbed, MkGenLet, MkCast,
+{-# COMPLETE MkAbs, MkApp, MkVar, MkSig, MkTyAbs, MkTyEmbed, MkLet, MkCast,
              MkZero, MkSucc, MkPair, MkFst, MkSnd,
             MkCase, MkNumFloat, MkNumInteger, MkStringConst, MkBinOp, 
              MkCon, MkCond #-}
-{-# COMPLETE Abs, App, Var, Sig, TyAbs, TyEmbed, GenLet, Cast,
+{-# COMPLETE Abs, App, Var, Sig, TyAbs, TyEmbed, Let, Cast,
              Zero, Succ, Pair, Fst, Snd,
              Case, NumFloat, NumInteger, StringConst, BinOp, Con, 
              Cond #-}
@@ -223,7 +231,7 @@ isValue e       = isNatVal e
 isNatVal :: Expr -> Bool
 isNatVal Zero = True
 isNatVal Succ = True
-isNatVal (App e1 e2) = isNatVal e1 && isNatVal e2
+isNatVal (App e1 es) = isNatVal e1 && all isNatVal es
 isNatVal _           = False
 
 ------------------------------
@@ -249,7 +257,7 @@ instance Ord (ProxyN n) where
 data Type (n :: Nat) where
     -- {id : arg1} -> arg2
     ImplicitFunTy :: Identifier -> Type 2 -> Type 1 -> Type 1
-    FunTy :: Type l -> Type l -> Type l  -- A -> B
+    FunTy :: [Type l] -> Type l -> Type l  -- A -> B
 
     TyCon :: ProxyN l -> Identifier -> Type l        -- K
 
@@ -301,13 +309,13 @@ class Term t where
   mkVar     :: Identifier -> t
 
 instance Term Expr where
-  boundVars (Abs var _ e)                = var `Set.insert` boundVars e
+  boundVars (Abs params e)               = Set.fromList (map fst params) `Set.union` boundVars e
   boundVars (TyAbs var e)                = var `Set.insert` boundVars e
   boundVars (TyEmbed t)                  = boundVars t
-  boundVars (App e1 e2)                  = boundVars e1 `Set.union` boundVars e2
+  boundVars (App e1 es)                  = boundVars e1 `Set.union` Set.unions (map boundVars es)
   boundVars (Var var)                    = Set.empty
   boundVars (Sig e _)                    = boundVars e
-  boundVars (GenLet var e1 e2)           = var `Set.insert` (boundVars e1 `Set.union` boundVars e2)
+  boundVars (Let var e1 e2)              = var `Set.insert` (boundVars e1 `Set.union` boundVars e2)
   boundVars (Cast e)                     = boundVars e
   boundVars (Pair e1 e2)                 = boundVars e1 `Set.union` boundVars e2
   boundVars (Fst e)                      = boundVars e
@@ -319,13 +327,13 @@ instance Term Expr where
   boundVars (Cond e1 e2 e3)              = boundVars e1 `Set.union` boundVars e2 `Set.union` boundVars e3
   boundVars _                            = Set.empty
 
-  freeVars (Abs var _ e)                 = Set.delete var (freeVars e)
+  freeVars (Abs params e)                = foldr Set.delete (freeVars e) (map fst params)
   freeVars (TyAbs var e)                 = Set.delete var (freeVars e)
   freeVars (TyEmbed t)                   = freeVars t
-  freeVars (App e1 e2)                   = freeVars e1 `Set.union` freeVars e2
+  freeVars (App e1 es)                   = freeVars e1 `Set.union` Set.unions (map freeVars es)
   freeVars (Var var)                     = Set.singleton var
   freeVars (Sig e _)                     = freeVars e
-  freeVars (GenLet var e1 e2)            = Set.delete var (freeVars e1 `Set.union` freeVars e2)
+  freeVars (Let var e1 e2)               = Set.delete var (freeVars e1 `Set.union` freeVars e2)
   freeVars (Cast e)                      = freeVars e
   freeVars (Pair e1 e2)                  = freeVars e1 `Set.union` freeVars e2
   freeVars (Fst e)                       = freeVars e
@@ -340,7 +348,7 @@ instance Term Expr where
   mkVar = Var
 
 instance {-# OVERLAPS #-} Term (Type 0) where
-  boundVars (FunTy t1 t2)  = boundVars t1 `Set.union` boundVars t2
+  boundVars (FunTy ts t2)  = Set.unions (map boundVars ts) `Set.union` boundVars t2
   boundVars (ProdTy t1 t2) = boundVars t1 `Set.union` boundVars t2
   boundVars (SumTy t1 t2)  = boundVars t1 `Set.union` boundVars t2
   boundVars (ImplicitTyApp t1 t2)  = boundVars t1 `Set.union` boundVars t2
@@ -351,7 +359,7 @@ instance {-# OVERLAPS #-} Term (Type 0) where
   boundVars (WithTy t1 t2) = boundVars t1 `Set.union` boundVars t2
   boundVars (ExponentTy t1 _) = boundVars t1
 
-  freeVars (FunTy t1 t2)  = freeVars t1 `Set.union` freeVars t2
+  freeVars (FunTy ts t2)  = Set.unions (map freeVars ts) `Set.union` freeVars t2
   freeVars (ProdTy t1 t2) = freeVars t1 `Set.union` freeVars t2
   freeVars (SumTy t1 t2)  = freeVars t1 `Set.union` freeVars t2
   freeVars (ImplicitTyApp t1 t2)  = freeVars t1 `Set.union` freeVars t2
@@ -366,14 +374,14 @@ instance {-# OVERLAPS #-} Term (Type 0) where
 
 instance Term (Type 1) where
   boundVars (ImplicitFunTy i t1 t2) = i `Set.insert` (boundVars t1 `Set.union` boundVars t2)
-  boundVars (FunTy t1 t2)  = boundVars t1 `Set.union` boundVars t2
+  boundVars (FunTy ts t2)  = Set.unions (map boundVars ts) `Set.union` boundVars t2
   boundVars (TyApp t1 t2)  = boundVars t1 `Set.union` boundVars t2
   boundVars (TyCon _ _)      = Set.empty
   boundVars (TyVar var)    = Set.empty
   boundVars (WithTy t1 t2) = boundVars t1 `Set.union` boundVars t2
 
   freeVars (ImplicitFunTy i t1 t2) = freeVars t1 `Set.union` (Set.delete i (freeVars t2))
-  freeVars (FunTy t1 t2)  = freeVars t1 `Set.union` freeVars t2
+  freeVars (FunTy ts t2)  = Set.unions (map freeVars ts) `Set.union` freeVars t2
   freeVars (TyApp t1 t2)  = freeVars t1 `Set.union` freeVars t2
   freeVars (TyCon _ _)      = Set.empty
   freeVars (TyVar var)    = Set.singleton var
@@ -382,13 +390,13 @@ instance Term (Type 1) where
   mkVar = TyVar
 
 instance Term (Type 2) where
-  boundVars (FunTy t1 t2)  = boundVars t1 `Set.union` boundVars t2
+  boundVars (FunTy ts t2)  = Set.unions (map boundVars ts) `Set.union` boundVars t2
   boundVars (TyApp t1 t2)  = boundVars t1 `Set.union` boundVars t2
   boundVars (TyCon _ _)      = Set.empty
   boundVars (TyVar var)    = Set.empty
   boundVars (WithTy t1 t2) = boundVars t1 `Set.union` boundVars t2
 
-  freeVars (FunTy t1 t2)  = freeVars t1 `Set.union` freeVars t2
+  freeVars (FunTy ts t2)  = Set.unions (map freeVars ts) `Set.union` freeVars t2
   freeVars (TyApp t1 t2)  = freeVars t1 `Set.union` freeVars t2
   freeVars (TyCon _ _)      = Set.empty
   freeVars (TyVar var)    = Set.singleton var
diff --git a/src/Lang/TypeError.hs b/src/Lang/TypeError.hs
index 45c3dae..4279497 100644
--- a/src/Lang/TypeError.hs
+++ b/src/Lang/TypeError.hs
@@ -53,6 +53,9 @@ data TypeError
   | FreeVariablesInAbstraction [Identifier]
   | TermLevelTypeAbstraction Identifier
   | TypeApplicationExpectsType
+
+  -- Program well-formedness errors
+  | WellFormednessError WellFormednessError
   
   -- Generic/contextual errors
   | ContextualError String
@@ -65,6 +68,11 @@ data TypeError
 
   deriving (Show)
 
+data WellFormednessError
+  = MissingParameterAnnotation Identifier
+  | DuplicateParameterAnnotation Identifier
+  deriving (Show)
+
 class MonadAlt m where
   (<|>) :: m a -> m a -> m a
 
diff --git a/src/Lang/Types.hs b/src/Lang/Types.hs
index 275db81..7923781 100644
--- a/src/Lang/Types.hs
+++ b/src/Lang/Types.hs
@@ -41,6 +41,10 @@ synthProgram = synthProgram' []
         Right ty -> synthProgram' ((v, ty) : gamma) defs
         Left err -> Left err
 
+    synthProgram' gamma ((FunDefElaborated v params body):defs) = do
+      params' <- traverse elaborateParameter params
+      (_, resultType) <- synthProgram' (params' ++ gamma) body
+      synthProgram' ((v, FunTy (map snd params') resultType) : gamma) defs
 
     synthProgram' gamma ((Return e):defs) = do
       ty <- synth gamma e
@@ -51,6 +55,10 @@ synthProgram = synthProgram' []
 
     synthProgram' gamma (_:defs) = synthProgram' gamma defs
 
+    elaborateParameter (name, ty) = do
+      ty' <- checkKind ty type0
+      return (name, ty')
+
 -- Represent contexts as lists
 type Context = [(Identifier, Type 0)]
 
@@ -100,9 +108,12 @@ check_ gamma (StringConst _) ty =
     _ -> Left $ TypeCheckFailure (integerTy unitDescription) ty "Expecting String type."
 
 check_ gamma (Sig e tyA) ty =
-  case typeEquality ty (IsSpec tyA) of
-    Right () -> check_ gamma e tyA
-    Left err -> Left $ TypeCheckFailure tyA ty (let ?srcFile = "" in errorToString err)
+  case checkKind tyA type0 of
+    Left err -> Left err
+    Right tyA' ->
+      case typeEquality ty (IsSpec tyA') of
+        Right () -> check_ gamma e tyA'
+        Left err -> Left $ TypeCheckFailure tyA' ty (let ?srcFile = "" in errorToString err)
 
 {--
 
@@ -111,15 +122,16 @@ G, x : A |- e <= B
 G |- (\x -> e) <= A -> B
 
 -}
--- Curry style
-check_ gamma (Abs x Nothing expr) (FunTy tyA tyB) =
-  check ([(x, tyA)] ++ gamma) expr tyB
-
--- Church style
-check_ gamma (Abs x (Just tyA') expr) (FunTy tyA tyB) =
-  case typeEquality tyA' (IsSpec tyA) of
-    Right () -> check ([(x, tyA)] ++ gamma) expr tyB
-    Left err -> Left $ ChainedError (FunctionAbstractionTypeMismatch tyA tyA') err
+-- Curry/Church style, mixed per-parameter. A n-ary function type can be
+-- matched either by one fully-applied abstraction or by nested abstractions
+-- taking fewer parameters at a time (currying).
+check_ gamma (Abs params expr) (FunTy tyAs tyB)
+  | length params <= length tyAs = do
+      let (tyAsHere, tyAsRest) = splitAt (length params) tyAs
+      typedParams <- checkAbsParams params tyAsHere
+      let remainingTy = if null tyAsRest then tyB else FunTy tyAsRest tyB
+      check (typedParams ++ gamma) expr remainingTy
+  | otherwise = Left $ ContextualError "Function abstraction has the wrong number of arguments"
 
 check_ gamma (Pair e1 e2) (ProdTy t1 t2) = do
   check gamma e1 t1
@@ -264,6 +276,12 @@ synth_ gamma (Var x) =
           Just ty -> Right ty
           Nothing -> Left $ VariableNotFound x
 
+synth_ _ (Con "()" []) = Right $ tyCon0 "()"
+
+synth_ gamma (Let x e1 e2) = do
+  ty1 <- synth gamma e1
+  synth ((x, ty1) : gamma) e2
+
 
 {-
 
@@ -284,7 +302,7 @@ i.e., we know we have a signature for the argument.
 -}
 
 -- app (special for form of top-level definitions)
-synth_ gamma (App (Abs x Nothing e1) (Sig e2 tyA)) =
+synth_ gamma (App (Abs [(x, Nothing)] e1) [Sig e2 tyA]) =
   case checkKind tyA type0 of
     Left err -> Left err
     Right tyA ->
@@ -294,15 +312,20 @@ synth_ gamma (App (Abs x Nothing e1) (Sig e2 tyA)) =
 
 
 -- abs-Church (actually rule)
-synth_ gamma (Abs x (Just tyA) e) =
-  case checkKind tyA type0 of
-    Left err -> Left err
-    Right tyA' -> do
-      tyB <- synth ((x, tyA') : gamma) e
-      Right (FunTy tyA' tyB)
+synth_ gamma (Abs params e)
+  | all (isJust . snd) params = do
+      typedParams <- traverse elaborateAbsParam params
+      tyB <- synth (typedParams ++ gamma) e
+      Right (FunTy (map snd typedParams) tyB)
+  | otherwise = Left $ CannotSynthType (Abs params e)
+  where
+    elaborateAbsParam (x, Just tyA) = do
+      tyA' <- checkKind tyA type0
+      return (x, tyA')
+    elaborateAbsParam (_, Nothing) = Left $ CannotSynthType (Abs params e)
 
 -- Type checking a type speciaisation
-synth_ gamma (App e (TyEmbed tau')) =
+synth_ gamma (App e [TyEmbed tau']) =
   case checkKind tau' type0 of
     Left err -> Left err
     Right tau' ->
@@ -322,7 +345,7 @@ synth_ gamma (App e (TyEmbed tau')) =
 -- special case primitive: sqrt
 -- infer the argument's description and halve every exponent in it,
 -- e.g. an argument described by [M^2] yields a result described by [M]
-synth_ gamma (App (Var "sqrt") e) = do
+synth_ gamma (App (Var "sqrt") [e]) = do
   t <- synth gamma e
   case isGradableNumericType t of
     Just ("Float", gradeType, d) -> do
@@ -330,14 +353,12 @@ synth_ gamma (App (Var "sqrt") e) = do
       Right $ TyApp (ImplicitTyApp (tyCon0 "Float") gradeType) d'
     _ -> Left $ ContextualError $ "sqrt expects a Float argument but got " <> pprint t
 
-synth_ gamma (App e1 e2) =
+synth_ gamma (App e1 es) =
   -- Synth the left-hand side
   case synth gamma e1 of
-    Right (FunTy tyA tyB) ->
-      -- Check the right-hand side
-      case check gamma e2 tyA of
-        Right () -> Right tyB
-        Left err -> Left err
+    Right (FunTy tys tyB) -> do
+      checkArguments gamma es tys
+      Right tyB
 
     Right t ->
       Left $ ExpectingFunctionType e1 t
@@ -349,7 +370,7 @@ synth_ gamma Zero =
   Right natTy
 
 synth_ gamma Succ =
-  Right (FunTy natTy natTy)
+  Right (FunTy [natTy] natTy)
 
 synth_ gamma (Pair e1 e2) =
   case synth gamma e1 of
@@ -511,6 +532,27 @@ synth_ gamma (Sig e ty) =
 synth_ gamma e =
    Left $ CannotSynthType e
 
+checkArguments :: Context -> [Expr] -> [Type 0] -> Either TypeError ()
+checkArguments gamma expressions types
+  | length expressions /= length types =
+      Left $ ContextualError "Function application has the wrong number of arguments"
+  | otherwise = sequence_ (zipWith (check gamma) expressions types)
+
+-- | Match each abstraction parameter (with an optional annotation) against
+-- its expected domain type, requiring annotations to agree when present.
+checkAbsParams :: [(Identifier, Maybe (Type 0))] -> [Type 0] -> Either TypeError Context
+checkAbsParams [] [] = Right []
+checkAbsParams ((x, Nothing):params) (tyA:tyAs) = do
+  rest <- checkAbsParams params tyAs
+  return ((x, tyA) : rest)
+checkAbsParams ((x, Just tyA'):params) (tyA:tyAs) =
+  case typeEquality tyA' (IsSpec tyA) of
+    Right () -> do
+      rest <- checkAbsParams params tyAs
+      return ((x, tyA) : rest)
+    Left err -> Left $ ChainedError (FunctionAbstractionTypeMismatch tyA tyA') err
+checkAbsParams _ _ = Left $ ContextualError "Function abstraction has the wrong number of arguments"
+
 ---------------------------------
 -- # Type equality
 ---------------------------------
@@ -674,6 +716,13 @@ errorToString (TermLevelTypeAbstraction alpha) =
 errorToString TypeApplicationExpectsType =
   "Type application expects a type"
 
+errorToString (WellFormednessError err) =
+  "Malformed program: " <> case err of
+    MissingParameterAnnotation parameter ->
+      "function parameter `" <> parameter <> "` has no type annotation"
+    DuplicateParameterAnnotation parameter ->
+      "function parameter `" <> parameter <> "` is annotated in both the header and body"
+
 errorToString (ContextualError msg) =
   msg
 
@@ -691,7 +740,7 @@ normalise t =
     else normalise (normalise' t)
 
 normalise' :: Type 0 -> Type 0
-normalise' (FunTy t1 t2) = FunTy (normalise' t1) (normalise' t2)
+normalise' (FunTy ts t2) = FunTy (map normalise' ts) (normalise' t2)
 normalise' (isGradableNumericType -> Just (baseType, gradeType, desc)) =
   TyApp (ImplicitTyApp (tyCon0 baseType) gradeType) (either (const desc) id (normalisationByEvaluation desc))
 normalise' (TyApp t1 t2) = TyApp (normalise' t1) (normalise' t2)
diff --git a/tests/Spec.hs b/tests/Spec.hs
index 3926ad2..629c5d7 100644
--- a/tests/Spec.hs
+++ b/tests/Spec.hs
@@ -19,6 +19,7 @@ import Control.Monad (unless)
 
 import qualified Lang.Frontend as Lang
 import Lang.Syntax
+import Lang.Semantics (Value(..), interpret, lookupBinding)
 import Lang.PrettyPrint (pprint)
 import Lang.Descriptions (normalisationByEvaluation, descriptionEquality)
 import Lang.TypeHelpers (Specificational(..))
@@ -30,7 +31,7 @@ import Test.Tasty.HUnit (testCase, (@?=), assertBool, assertFailure)
 import Debug.Trace
 
 type InterpreterError = String
-type InterpreterResult = Expr
+type InterpreterResult = Value
 
 
 
@@ -41,7 +42,7 @@ main = do
   positive  <- goldenTestsPositive
 
   catch
-    (defaultMain $ testGroup "All tests" [negative, positive, speciesUnitTests, basisUnitTests])
+    (defaultMain $ testGroup "All tests" [negative, positive, speciesUnitTests, basisUnitTests, applicationUnitTests])
     (\(e :: ExitCode) -> do
       throwIO e
     )
@@ -66,7 +67,7 @@ goldenTestsNegative = do
     formatResult :: Either InterpreterError InterpreterResult -> String
     formatResult = \case
         Left err -> err
-        Right x -> error $ "Negative test passed!\n" <> show x
+        Right x -> error $ "Negative test passed!\n" <> pprint x
 
 goldenTestsPositive :: IO TestTree
 goldenTestsPositive = do
@@ -128,6 +129,46 @@ failOnOrphanOutfiles files outfiles
 fortlFileExtensions :: [String]
 fortlFileExtensions = [".frtl"]
 
+-- Unit tests for closure under-/over-application. These are exercised at the
+-- interpreter level directly because the typechecker requires exact arity.
+applicationUnitTests :: TestTree
+applicationUnitTests = testGroup "Closure application unit tests"
+  [ testCase "under-application yields a closure awaiting the remaining parameters" $
+      case lookupBinding "partial" (fst (interpret [] underProg)) of
+        Right (VClosure params _ _) -> params @?= ["y"]
+        Right v  -> assertFailure ("Expected a closure but got " <> pprint v)
+        Left err -> assertFailure err
+  , testCase "under-applied closure completes when given the remaining argument" $
+      assertEvalsTo (underProg ++ [Return (App (Var "partial") [NumFloat 2.0])]) 3.0
+  , testCase "over-application applies leftover arguments to the returned closure" $
+      assertEvalsTo [adderDef, Return (App (Var "adder") [NumFloat 1.0, NumFloat 2.0])] 3.0
+  ]
+  where
+    fl = tyCon0 "Float"
+
+    -- def add(x, y): return x + y
+    -- partial = add(1.0)
+    underProg =
+      [ FunDefElaborated "add" [("x", fl), ("y", fl)]
+          [Return (BinOp BinOpPlus (Var "x") (Var "y"))]
+      , ValDef (VarLhs "partial" Nothing) (App (Var "add") [NumFloat 1.0])
+      ]
+
+    -- def adder(x):
+    --   def inner(y): return x + y
+    --   return inner
+    adderDef =
+      FunDefElaborated "adder" [("x", fl)]
+        [ FunDefElaborated "inner" [("y", fl)]
+            [Return (BinOp BinOpPlus (Var "x") (Var "y"))]
+        , Return (Var "inner")
+        ]
+
+    assertEvalsTo prog expected =
+      case snd (interpret [] prog) of
+        ValExpr (NumFloat n) -> n @?= expected
+        v -> assertFailure ("Expected " <> show expected <> " but got " <> pprint v)
+
 -- Unit tests for species indexing semantics
 speciesUnitTests :: TestTree
 speciesUnitTests = testGroup "Species indexing unit tests"
diff --git a/tests/cases/negative/duplicate-parameter-annotation.frtl b/tests/cases/negative/duplicate-parameter-annotation.frtl
new file mode 100644
index 0000000..a903ce5
--- /dev/null
+++ b/tests/cases/negative/duplicate-parameter-annotation.frtl
@@ -0,0 +1,5 @@
+def identity(x: Float[Unit[1]]):
+  x : Float[Unit[1]]
+  return x
+
+it = identity((1.0 : Float[Unit[1]]))
\ No newline at end of file
diff --git a/tests/cases/negative/duplicate-parameter-annotation.frtl.output b/tests/cases/negative/duplicate-parameter-annotation.frtl.output
new file mode 100644
index 0000000..3d00c64
--- /dev/null
+++ b/tests/cases/negative/duplicate-parameter-annotation.frtl.output
@@ -0,0 +1 @@
+Malformed program: function parameter `x` is annotated in both the header and body
\ No newline at end of file
diff --git a/tests/cases/negative/label-conflict.frtl.output b/tests/cases/negative/label-conflict.frtl.output
new file mode 100644
index 0000000..e2e7ed9
--- /dev/null
+++ b/tests/cases/negative/label-conflict.frtl.output
@@ -0,0 +1 @@
+tests/cases/negative/label-conflict.frtl:2:5: Overlapping descriptor key `Unit` conflicts: Unit[m] vs Unit[s]
\ No newline at end of file
diff --git a/tests/cases/negative/missing-parameter-annotation.frtl b/tests/cases/negative/missing-parameter-annotation.frtl
new file mode 100644
index 0000000..fcea1dc
--- /dev/null
+++ b/tests/cases/negative/missing-parameter-annotation.frtl
@@ -0,0 +1,4 @@
+def identity(x):
+  return x
+
+it = identity(1.0)
\ No newline at end of file
diff --git a/tests/cases/negative/missing-parameter-annotation.frtl.output b/tests/cases/negative/missing-parameter-annotation.frtl.output
new file mode 100644
index 0000000..b9b0ab6
--- /dev/null
+++ b/tests/cases/negative/missing-parameter-annotation.frtl.output
@@ -0,0 +1 @@
+Malformed program: function parameter `x` has no type annotation
\ No newline at end of file
diff --git a/tests/cases/positive/def-body-annotation.frtl b/tests/cases/positive/def-body-annotation.frtl
new file mode 100644
index 0000000..bb55212
--- /dev/null
+++ b/tests/cases/positive/def-body-annotation.frtl
@@ -0,0 +1,7 @@
+def increment(x):
+  x : Float[Unit[1]]
+  result : Float[Unit[1]]
+  result = x + (1.0 : Float[Unit[1]])
+  return result
+
+it : Float[Unit[1]] = increment((2.0 : Float[Unit[1]]))
\ No newline at end of file
diff --git a/tests/cases/positive/def-body-annotation.frtl.output b/tests/cases/positive/def-body-annotation.frtl.output
new file mode 100644
index 0000000..f398a20
--- /dev/null
+++ b/tests/cases/positive/def-body-annotation.frtl.output
@@ -0,0 +1 @@
+3.0
\ No newline at end of file
diff --git a/tests/cases/positive/def-functions.frtl b/tests/cases/positive/def-functions.frtl
new file mode 100644
index 0000000..d3cfeed
--- /dev/null
+++ b/tests/cases/positive/def-functions.frtl
@@ -0,0 +1,5 @@
+def add(x: Float[1], y: Float[1]):
+  result = x + y
+  return result
+
+it : Float[1] = add(2.0, 3.0)
\ No newline at end of file
diff --git a/tests/cases/positive/def-functions.frtl.output b/tests/cases/positive/def-functions.frtl.output
new file mode 100644
index 0000000..6e63660
--- /dev/null
+++ b/tests/cases/positive/def-functions.frtl.output
@@ -0,0 +1 @@
+5.0
\ No newline at end of file
diff --git a/tests/cases/positive/nested_fun.py b/tests/cases/positive/nested_fun.py
new file mode 100644
index 0000000..470c585
--- /dev/null
+++ b/tests/cases/positive/nested_fun.py
@@ -0,0 +1,10 @@
+def g():
+  def f():
+    return 100
+  return f
+
+def f():
+    return 42
+
+fun = g()
+it = fun()
\ No newline at end of file