diff --git a/fco2/AST.hs b/fco2/AST.hs
index b02df22..a8f08e1 100644
--- a/fco2/AST.hs
+++ b/fco2/AST.hs
@@ -24,7 +24,8 @@ data NameDef = NameDef {
     ndMeta :: Meta,
     ndName :: String,
     ndOrigName :: String,
-    ndType :: SpecType
+    ndType :: SpecType,
+    ndAbbrevMode :: AbbrevMode
   }
   deriving (Show, Eq, Typeable, Data)
 
@@ -42,7 +43,6 @@ data Type =
   | Any
   | Timer
   | Port Type
-  | Val Type
   | Infer   -- for where the type is not given but can be worked out (e.g. "x IS y:")
   | NoType  -- for where we need a Type, but none exists (e.g. PROCs scoping in)
   deriving (Show, Eq, Typeable, Data)
@@ -173,25 +173,31 @@ data InputMode =
   | InputAfter Meta Expression
   deriving (Show, Eq, Typeable, Data)
 
-type Formals = [(Type, Name)]
+data AbbrevMode =
+  Abbrev
+  | ValAbbrev
+  deriving (Show, Eq, Typeable, Data)
+
 type Specification = (Name, SpecType)
 data SpecType =
   Place Meta Expression
   | Declaration Meta Type
-  | Is Meta Type Variable
-  | ValIs Meta Type Expression
+  | Is Meta AbbrevMode Type Variable
+  | IsExpr Meta AbbrevMode Type Expression
   | IsChannel Meta Type Channel
   | IsChannelArray Meta Type [Channel]
   | DataType Meta Type
   | DataTypeRecord Meta Bool [(Type, Name)]
   | Protocol Meta [Type]
   | ProtocolCase Meta [(Name, [Type])]
-  | Proc Meta Formals Process
-  | Function Meta [Type] Formals ValueProcess
-  | Retypes Meta Type Variable
-  | Reshapes Meta Type Variable
-  | ValRetypes Meta Type Variable
-  | ValReshapes Meta Type Variable
+  | Proc Meta [Formal] Process
+  | Function Meta [Type] [Formal] ValueProcess
+  | Retypes Meta AbbrevMode Type Variable
+  | RetypesExpr Meta AbbrevMode Type Expression
+  deriving (Show, Eq, Typeable, Data)
+
+data Formal =
+  Formal AbbrevMode Type Name
   deriving (Show, Eq, Typeable, Data)
 
 data Actual =
diff --git a/fco2/GenerateC.hs b/fco2/GenerateC.hs
index b527642..bcdd4fc 100644
--- a/fco2/GenerateC.hs
+++ b/fco2/GenerateC.hs
@@ -14,9 +14,6 @@ module GenerateC where
 -- FIXME: There should be a pass that pulls PAR branches (that aren't already
 -- PROC calls) out into PROCs.
 
--- FIXME: Val shouldn't be part of the type -- it's part of the *abbeviation*.
--- That is, we should have an AbbreviationMode (which can also do RESULT etc. later).
-
 -- FIXME: Arrays. Should be a struct that contains the data and size, and we
 -- then use a pointer to the struct to pass around.
 
@@ -97,12 +94,15 @@ genType (ArrayUnsized t)
 genType (UserDataType n) = genName n
 genType (Chan t)
     =  do tell ["Channel*"]
-genType (Val t)
-    =  do tell ["const "]
-          genType t
 genType t = missing $ "genType " ++ show t
 --}}}
 
+--{{{  abbreviations
+genConst :: AbbrevMode -> CGen ()
+genConst Abbrev = return ()
+genConst ValAbbrev = tell ["const "]
+--}}}
+
 --{{{  conversions
 genConversion :: ConversionMode -> Type -> Expression -> CGen ()
 genConversion DefaultConversion t e
@@ -353,15 +353,16 @@ introduceSpec (n, Declaration m t)
                     tell [" "]
                     genName n
                     tell [";\n"]
-introduceSpec (n, Is m t v)
-    =  do genType t
+introduceSpec (n, Is m am t v)
+    =  do genConst am
+          genType t
           tell ["& "]
           genName n
           tell [" = "]
           genVariable v
           tell [";\n"]
-introduceSpec (n, ValIs m t e)
-    =  do tell ["const "]
+introduceSpec (n, IsExpr m am t e)
+    =  do genConst am
           genType t
           tell [" "]
           genName n
@@ -405,21 +406,19 @@ genActual :: Actual -> CGen ()
 genActual (ActualExpression e) = genExpression e
 genActual (ActualChannel c) = genChannel c
 
-genFormals :: Formals -> CGen ()
+genFormals :: [Formal] -> CGen ()
 genFormals fs = sequence_ $ intersperse genComma (map genFormal fs)
 
 -- Arrays must be handled specially
-genFormal :: (Type, Name) -> CGen ()
-genFormal (ft, n)
-    =  do case ft of
-            Val t ->
-              do tell ["const "]
+genFormal :: Formal -> CGen ()
+genFormal (Formal am t n)
+    =  do case am of
+            ValAbbrev ->
+              do genConst am
                  genType t
                  tell [" "]
-            Chan t ->
-              tell ["Channel *"]
-            _ ->
-              do genType ft
+            Abbrev ->
+              do genType t
                  tell ["& "]
           genName n
 --}}}
diff --git a/fco2/Parse.hs b/fco2/Parse.hs
index 36d878b..fb0d43d 100644
--- a/fco2/Parse.hs
+++ b/fco2/Parse.hs
@@ -287,8 +287,8 @@ findName thisN
             then fail $ "expected " ++ show (A.nameType thisN) ++ " (" ++ A.nameName origN ++ " is " ++ show (A.nameType origN) ++ ")"
             else return $ thisN { A.nameName = A.nameName origN }
 
-scopeIn :: A.Name -> A.SpecType -> OccParser A.Name
-scopeIn n@(A.Name m nt s) t
+scopeIn :: A.Name -> A.SpecType -> A.AbbrevMode -> OccParser A.Name
+scopeIn n@(A.Name m nt s) t am
     =  do st <- getState
           let s' = s ++ "_" ++ (show $ psNameCounter st)
           let n' = n { A.nameName = s' }
@@ -296,7 +296,8 @@ scopeIn n@(A.Name m nt s) t
             A.ndMeta = m,
             A.ndName = s',
             A.ndOrigName = s,
-            A.ndType = t
+            A.ndType = t,
+            A.ndAbbrevMode = am
           }
           setState $ st {
             psNameCounter = (psNameCounter st) + 1,
@@ -316,7 +317,7 @@ scopeOut n@(A.Name m nt s)
 -- FIXME: Do these with generics? (going carefully to avoid nested code blocks)
 scopeInRep :: A.Replicator -> OccParser A.Replicator
 scopeInRep r@(A.For m n b c)
-    =  do n' <- scopeIn n (A.Declaration m A.Int)
+    =  do n' <- scopeIn n (A.Declaration m A.Int) A.ValAbbrev
           return $ A.For m n' b c
 
 scopeOutRep :: A.Replicator -> OccParser ()
@@ -324,24 +325,22 @@ scopeOutRep r@(A.For m n b c) = scopeOut n
 
 scopeInSpec :: A.Specification -> OccParser A.Specification
 scopeInSpec s@(n, st)
-    =  do n' <- scopeIn n st
+    =  do n' <- scopeIn n st (abbrevModeOfSpec st)
           return (n', st)
 
 scopeOutSpec :: A.Specification -> OccParser ()
 scopeOutSpec s@(n, st) = scopeOut n
 
-scopeInFormal :: (A.Type, A.Name) -> OccParser (A.Type, A.Name)
-scopeInFormal (t, n)
-    =  do n' <- scopeIn n (A.Declaration (A.nameMeta n) t)
-          return (t, n')
+scopeInFormal :: A.Formal -> OccParser A.Formal
+scopeInFormal (A.Formal am t n)
+    =  do n' <- scopeIn n (A.Declaration (A.nameMeta n) t) am
+          return (A.Formal am t n')
 
-scopeInFormals :: A.Formals -> OccParser A.Formals
+scopeInFormals :: [A.Formal] -> OccParser [A.Formal]
 scopeInFormals fs = mapM scopeInFormal fs
 
-scopeOutFormals :: A.Formals -> OccParser ()
-scopeOutFormals fs
-    =  do _ <- mapM scopeOut (map snd fs)
-          return ()
+scopeOutFormals :: [A.Formal] -> OccParser ()
+scopeOutFormals fs = sequence_ [scopeOut n | (A.Formal am t n) <- fs]
 
 --}}}
 
@@ -724,11 +723,11 @@ declaration
 
 abbreviation :: OccParser A.Specification
 abbreviation
-    =   try (do { m <- md; n <- newVariableName; sIS; v <- variable; sColon; eol; return (n, A.Is m A.Infer v) })
-    <|> try (do { m <- md; s <- specifier; n <- newVariableName; sIS; v <- variable; sColon; eol; return (n, A.Is m s v) })
+    =   try (do { m <- md; n <- newVariableName; sIS; v <- variable; sColon; eol; return (n, A.Is m A.Abbrev A.Infer v) })
+    <|> try (do { m <- md; s <- specifier; n <- newVariableName; sIS; v <- variable; sColon; eol; return (n, A.Is m A.Abbrev s v) })
     <|> do { m <- md; sVAL ;
-              try (do { n <- newVariableName; sIS; e <- expression; sColon; eol; return (n, A.ValIs m A.Infer e) })
-              <|> do { s <- specifier; n <- newVariableName; sIS; e <- expression; sColon; eol; return (n, A.ValIs m s e) } }
+              try (do { n <- newVariableName; sIS; e <- expression; sColon; eol; return (n, A.IsExpr m A.ValAbbrev A.Infer e) })
+              <|> do { s <- specifier; n <- newVariableName; sIS; e <- expression; sColon; eol; return (n, A.IsExpr m A.ValAbbrev s e) } }
     <|> try (do { m <- md; n <- newChannelName <|> newTimerName <|> newPortName; sIS; c <- channel; sColon; eol; return (n, A.IsChannel m A.Infer c) })
     <|> try (do { m <- md; s <- specifier; n <- newChannelName <|> newTimerName <|> newPortName; sIS; c <- channel; sColon; eol; return (n, A.IsChannel m s c) })
     <|> try (do { m <- md; n <- newChannelName; sIS; sLeft; cs <- sepBy1 channel sComma; sRight; sColon; eol; return (n, A.IsChannelArray m A.Infer cs) })
@@ -748,11 +747,9 @@ definition
                   do { sIS; fs' <- scopeInFormals fs; el <- expressionList; scopeOutFormals fs'; sColon; eol; return (n, A.Function m rs fs' (A.ValOf m (A.Skip m) el)) }
                   <|> do { eol; indent; fs' <- scopeInFormals fs; vp <- valueProcess; scopeOutFormals fs'; outdent; sColon; eol; return (n, A.Function m rs fs' vp) } })
     <|> try (do { m <- md; s <- specifier; n <- newVariableName ;
-                  do { sRETYPES; v <- variable; sColon; eol; return (n, A.Retypes m s v) }
-                  <|> do { try sRESHAPES; v <- variable; sColon; eol; return (n, A.Reshapes m s v) } })
+                  sRETYPES <|> sRESHAPES; v <- variable; sColon; eol; return (n, A.Retypes m A.Abbrev s v) })
     <|> do {  m <- md; sVAL; s <- specifier; n <- newVariableName ;
-              do { sRETYPES; v <- variable; sColon; eol; return (n, A.ValRetypes m s v) }
-              <|> do { sRESHAPES; v <- variable; sColon; eol; return (n, A.ValReshapes m s v) } }
+              sRETYPES <|> sRESHAPES; e <- expression; sColon; eol; return (n, A.RetypesExpr m A.ValAbbrev s e) }
     <?> "definition"
 
 dataSpecifier :: OccParser A.Type
@@ -771,7 +768,7 @@ specifier
     <?> "specifier"
 
 --{{{ PROCs and FUNCTIONs
-formalList :: OccParser A.Formals
+formalList :: OccParser [A.Formal]
 formalList
     =  do m <- md
           sLeftR
@@ -780,22 +777,22 @@ formalList
           return $ concat fs
     <?> "formalList"
 
-formalArgSet :: OccParser A.Formals
+formalArgSet :: OccParser [A.Formal]
 formalArgSet
-    =   try (do t <- formalVariableType
+    =   try (do (am, t) <- formalVariableType
                 ns <- sepBy1NE newVariableName sComma
-                return [(t, n) | n <- ns])
+                return [A.Formal am t n | n <- ns])
     <|> do t <- specifier
            ns <- sepBy1NE newChannelName sComma
-           return [(t, n) | n <- ns]
+           return [A.Formal A.Abbrev t n | n <- ns]
     <?> "formalArgSet"
 
-formalVariableType :: OccParser A.Type
-    =   try (do { sVAL; s <- dataSpecifier; return $ A.Val s })
-    <|> dataSpecifier
+formalVariableType :: OccParser (A.AbbrevMode, A.Type)
+    =   try (do { sVAL; s <- dataSpecifier; return (A.ValAbbrev, s) })
+    <|> do { s <- dataSpecifier; return (A.Abbrev, s) }
     <?> "formalVariableType"
 
-functionHeader :: OccParser (A.Name, A.Formals)
+functionHeader :: OccParser (A.Name, [A.Formal])
 functionHeader
     =   do { sFUNCTION; n <- newFunctionName; fs <- formalList; return $ (n, fs) }
     <?> "functionHeader"
diff --git a/fco2/Types.hs b/fco2/Types.hs
index f867368..9bba281 100644
--- a/fco2/Types.hs
+++ b/fco2/Types.hs
@@ -21,19 +21,15 @@ typeOfName :: ParseState -> A.Name -> Maybe A.Type
 typeOfName ps n
     = case specTypeOfName ps n of
         Just (A.Declaration m t) -> Just t
-        Just (A.Is m t v) -> typeOfVariable ps v
-        Just (A.ValIs m t e) -> typeOfExpression ps e `perhaps` A.Val
+        Just (A.Is m am t v) -> typeOfVariable ps v
         Just (A.IsChannel m t c) -> typeOfChannel ps c
         Just (A.IsChannelArray m t (c:_)) -> typeOfChannel ps c `perhaps` A.ArrayUnsized
-        Just (A.Retypes m t v) -> Just t
-        Just (A.Reshapes m t v) -> Just t
-        Just (A.ValRetypes m t v) -> Just (A.Val t)
-        Just (A.ValReshapes m t v) -> Just (A.Val t)
+        Just (A.Retypes m am t v) -> Just t
+        Just (A.RetypesExpr m am t e) -> Just t
         _ -> Nothing
 
 -- FIXME: This should fail if the subscript is invalid...
 subscriptType :: A.Type -> Maybe A.Type
-subscriptType (A.Val t) = subscriptType t `perhaps` A.Val
 subscriptType (A.Array e t) = Just t
 subscriptType (A.ArrayUnsized t) = Just t
 subscriptType _ = Nothing
@@ -57,7 +53,7 @@ typeOfExpression ps e
         A.MostNeg m t -> Just t
         A.Size m t -> Just A.Int
         A.Conversion m cm t e -> Just t
-        A.ExprVariable m v -> typeOfVariable ps v `perhaps` noVal
+        A.ExprVariable m v -> typeOfVariable ps v
         A.ExprLiteral m l -> typeOfLiteral ps l
         A.True m -> Just A.Bool
         A.False m -> Just A.Bool
@@ -89,7 +85,14 @@ isCaseProtocolType ps (A.Chan (A.UserProtocol pr))
         _ -> False
 isCaseProtocolType ps _ = False
 
-noVal :: A.Type -> A.Type
-noVal (A.Val t) = t
-noVal t = t
+abbrevModeOfSpec :: A.SpecType -> A.AbbrevMode
+abbrevModeOfSpec s
+    = case s of
+        A.Is _ am _ _ -> am
+        A.IsExpr _ am _ _ -> am
+        A.IsChannel _ _ _ -> A.Abbrev
+        A.IsChannelArray _ _ _ -> A.Abbrev
+        A.Retypes _ am _ _ -> am
+        A.RetypesExpr _ am _ _ -> am
+        _ -> A.ValAbbrev