diff --git a/common/Types.hs b/common/Types.hs
index 58f76ac..535d0f6 100644
--- a/common/Types.hs
+++ b/common/Types.hs
@@ -20,7 +20,8 @@ with this program.  If not, see <http://www.gnu.org/licenses/>.
 module Types
   (
     specTypeOfName, typeOfSpec, abbrevModeOfName, typeOfName, typeOfExpression, typeOfVariable, underlyingType, stripArrayType, abbrevModeOfVariable, abbrevModeOfSpec
-    , isRealType, isIntegerType, isCaseableType, isScalarType, resolveUserType, isSafeConversion, isPreciseConversion, isImplicitConversionRain
+    , isRealType, isIntegerType, isNumericType, isCaseableType, isScalarType, isCommunicableType, isSequenceType
+    , resolveUserType, isSafeConversion, isPreciseConversion, isImplicitConversionRain
     , returnTypesOfFunction
     , BytesInResult(..), bytesInType, countReplicator, countStructured, computeStructured
 
@@ -472,6 +473,7 @@ isIntegerType t
         A.Int16 -> True
         A.Int32 -> True
         A.Int64 -> True
+        A.Time -> True
         _ -> False
 
 -- | Scalar real types.
@@ -482,6 +484,10 @@ isRealType t
         A.Real64 -> True
         _ -> False
 
+-- | Numeric types.
+isNumericType :: A.Type -> Bool
+isNumericType t = isIntegerType t || isRealType t
+
 -- | Types that are permitted as 'Case' selectors.
 isCaseableType :: A.Type -> Bool
 isCaseableType A.Bool = True
@@ -491,6 +497,21 @@ isCaseableType t = isIntegerType t
 isScalarType :: A.Type -> Bool
 isScalarType A.Bool = True
 isScalarType t = isIntegerType t || isRealType t
+
+-- | Types that can be communicated across a channel.
+isCommunicableType :: A.Type -> Bool
+isCommunicableType (A.Array _ t) = isCommunicableType t
+isCommunicableType (A.List t) = isCommunicableType t
+isCommunicableType (A.Record _) = True
+isCommunicableType (A.Mobile _) = True
+isCommunicableType t = isScalarType t
+
+-- | Types that support 'Size' and subscripting.
+isSequenceType :: A.Type -> Bool
+isSequenceType (A.Array _ _) = True
+isSequenceType (A.List _) = True
+isSequenceType _ = False
+
 --}}}
 
 --{{{ sizes of types
diff --git a/frontends/OccamTypes.hs b/frontends/OccamTypes.hs
index decfc71..0e143a2 100644
--- a/frontends/OccamTypes.hs
+++ b/frontends/OccamTypes.hs
@@ -89,29 +89,33 @@ checkType m et rt
     bad :: PassM ()
     bad = diePC m $ formatCode "Type mismatch: found %, expected %" rt et
 
+-- | Check a type against a predicate.
+checkTypeClass :: (A.Type -> Bool) -> String -> Meta -> A.Type -> PassM ()
+checkTypeClass f adjective m rawT
+    =  do t <- underlyingType m rawT
+          if f t
+            then ok
+            else diePC m $ formatCode ("Expected " ++ adjective ++ " type; found %") t
+
 -- | Check that a type is numeric.
 checkNumeric :: Meta -> A.Type -> PassM ()
-checkNumeric m rawT
-    =  do t <- underlyingType m rawT
-          if isIntegerType t || isRealType t
-            then ok
-            else diePC m $ formatCode "Expected numeric type; found %" t
+checkNumeric = checkTypeClass isNumericType "numeric"
 
 -- | Check that a type is integral.
 checkInteger :: Meta -> A.Type -> PassM ()
-checkInteger m rawT
-    =  do t <- underlyingType m rawT
-          if isIntegerType t
-            then ok
-            else diePC m $ formatCode "Expected integer type; found %" t
+checkInteger = checkTypeClass isIntegerType "integer"
 
 -- | Check that a type is scalar.
 checkScalar :: Meta -> A.Type -> PassM ()
-checkScalar m rawT
-    =  do t <- underlyingType m rawT
-          if isScalarType t
-            then ok
-            else diePC m $ formatCode "Expected scalar type; found %" t
+checkScalar = checkTypeClass isScalarType "scalar"
+
+-- | Check that a type is communicable.
+checkCommunicable :: Meta -> A.Type -> PassM ()
+checkCommunicable = checkTypeClass isCommunicableType "communicable"
+
+-- | Check that a type is a sequence.
+checkSequence :: Meta -> A.Type -> PassM ()
+checkSequence = checkTypeClass isSequenceType "array or list"
 
 -- | Check that a type is an array.
 -- (This also gets used elsewhere where we *know* the argument isn't an array,
@@ -120,15 +124,16 @@ checkArray :: Meta -> A.Type -> PassM ()
 checkArray m rawT
     =  do t <- underlyingType m rawT
           case t of
-            (A.Array _ _) -> ok
+            A.Array _ _ -> ok
             _ -> diePC m $ formatCode "Expected array type; found %" t
 
 -- | Check that a type is a list.
+-- Return the element type of the list.
 checkList :: Meta -> A.Type -> PassM ()
 checkList m rawT
     =  do t <- underlyingType m rawT
           case t of
-            (A.List _) -> ok
+            A.List _ -> ok
             _ -> diePC m $ formatCode "Expected list type; found %" t
 
 -- | Check the type of an expression.
@@ -184,11 +189,10 @@ checkSubscriptType m s rawT
             -- A record subscript.
             A.SubscriptField m n ->
               checkRecordField m t n
-            -- An array subscript.
-            _ ->
-              case t of
-                A.Array _ _ -> ok
-                _ -> checkArray m t
+            -- A sequence subscript.
+            A.Subscript _ _ _ -> checkSequence m t
+            -- An array slice.
+            _ -> checkArray m t
 
 -- | Classes of operators.
 data OpClass = NumericOp | IntegerOp | ShiftOp | BooleanOp | ComparisonOp
@@ -308,6 +312,15 @@ checkAllocMobile m rawT me
     checkFullDimension A.UnknownDimension
         = dieP m $ "Type in allocation contains unknown dimensions"
     checkFullDimension _ = ok
+
+-- | Check that a variable is writable.
+checkWritable :: A.Variable -> PassM ()
+checkWritable v
+    =  do am <- abbrevModeOfVariable v
+          case am of
+            A.ValAbbrev -> dieP (findMeta v) $ "Expected a writable variable"
+            _ -> ok
+
 --}}}
 
 -- | Check the AST for type consistency.
@@ -318,7 +331,11 @@ checkTypes t =
     checkSubscripts t >>=
     checkLiterals >>=
     checkVariables >>=
-    checkExpressions
+    checkExpressions >>=
+    checkInputItems >>=
+    checkOutputItems >>=
+    checkReplicators >>=
+    checkChoices
 
 checkSubscripts :: Data t => t -> PassM t
 checkSubscripts = checkDepthM doSubscript
@@ -383,13 +400,13 @@ checkExpressions = checkDepthM doExpression
     doExpression (A.Dyadic _ op le re) = checkDyadicOp op le re
     doExpression (A.MostPos m t) = checkNumeric m t
     doExpression (A.MostNeg m t) = checkNumeric m t
-    doExpression (A.SizeType m t) = checkArray m t
+    doExpression (A.SizeType m t) = checkSequence m t
     doExpression (A.SizeExpr m e)
         =  do t <- typeOfExpression e
-              checkArray m t
+              checkSequence m t
     doExpression (A.SizeVariable m v)
         =  do t <- typeOfVariable v
-              checkArray m t
+              checkSequence m t
     doExpression (A.Conversion m _ t e)
         =  do et <- typeOfExpression e
               checkScalar m t >> checkScalar (findMeta e) et
@@ -405,3 +422,52 @@ checkExpressions = checkDepthM doExpression
               checkRecordField m t n
     doExpression (A.AllocMobile m t me) = checkAllocMobile m t me
     doExpression _ = ok
+
+checkInputItems :: Data t => t -> PassM t
+checkInputItems = checkDepthM doInputItem
+  where
+    doInputItem :: A.InputItem -> PassM ()
+    doInputItem (A.InCounted m cv av)
+        =  do ct <- typeOfVariable cv
+              checkInteger (findMeta cv) ct
+              checkWritable cv
+              at <- typeOfVariable av
+              checkArray (findMeta av) at
+              checkCommunicable (findMeta av) at
+              checkWritable av
+    doInputItem (A.InVariable _ v)
+        =  do t <- typeOfVariable v
+              checkCommunicable (findMeta v) t
+              checkWritable v
+
+checkOutputItems :: Data t => t -> PassM t
+checkOutputItems = checkDepthM doOutputItem
+  where
+    doOutputItem :: A.OutputItem -> PassM ()
+    doOutputItem (A.OutCounted m ce ae)
+        =  do ct <- typeOfExpression ce
+              checkInteger (findMeta ce) ct
+              at <- typeOfExpression ae
+              checkArray (findMeta ae) at
+              checkCommunicable (findMeta ae) at
+    doOutputItem (A.OutExpression _ e)
+        =  do t <- typeOfExpression e
+              checkCommunicable (findMeta e) t
+
+checkReplicators :: Data t => t -> PassM t
+checkReplicators = checkDepthM doReplicator
+  where
+    doReplicator :: A.Replicator -> PassM ()
+    doReplicator (A.For _ _ start count)
+        =  do checkExpressionInt (findMeta start) start
+              checkExpressionInt (findMeta count) count
+    doReplicator (A.ForEach _ _ e)
+        =  do t <- typeOfExpression e
+              checkSequence (findMeta e) t
+
+checkChoices :: Data t => t -> PassM t
+checkChoices = checkDepthM doChoice
+  where
+    doChoice :: A.Choice -> PassM ()
+    doChoice (A.Choice _ e _) = checkExpressionBool (findMeta e) e
+
diff --git a/frontends/OccamTypesTest.hs b/frontends/OccamTypesTest.hs
index f558699..7e7df4b 100644
--- a/frontends/OccamTypesTest.hs
+++ b/frontends/OccamTypesTest.hs
@@ -37,21 +37,20 @@ m = emptyMeta
 -- | Initial state for the tests.
 startState :: State CompState ()
 startState
-    =  do defineConst "const" A.Int (intLiteral 2)
-          defineConst "someInt" A.Int (intLiteral 42)
-          defineConst "someByte" A.Byte (byteLiteral 24)
-          defineConst "someInts" (A.Array [A.UnknownDimension] A.Int)
-                      (A.Literal m (A.Array [A.UnknownDimension] A.Int)
-                                   (A.ArrayLiteral m []))
-          defineConst "someBytes" (A.Array [A.UnknownDimension] A.Byte)
-                      (A.Literal m (A.Array [A.UnknownDimension] A.Int)
-                                   (A.ArrayLiteral m []))
+    =  do defineConst "constInt" A.Int (intLiteral 2)
+          defineConst "constInts" intsT (A.Literal m intsT arrayLit)
+          defineVariable "varInt" A.Int
+          defineVariable "varByte" A.Byte
+          defineVariable "varReal" A.Real32
+          defineVariable "varInts" (A.Array [A.UnknownDimension] A.Int)
+          defineVariable "varBytes" (A.Array [A.UnknownDimension] A.Byte)
           defineUserDataType "MYINT" A.Int
           defineUserDataType "MY2INT" (A.Array [dimension 2] A.Int)
           defineRecordType "COORD2" [("x", A.Int), ("y", A.Int)]
           defineRecordType "COORD3" [("x", A.Real32), ("y", A.Real32),
                                      ("z", A.Real32)]
-          defineChannel "chanInt" (A.Chan A.DirUnknown ca A.Int)
+          defineChannel "chanInt" chanIntT
+          defineChannel "chansInt" (A.Array [A.UnknownDimension] chanIntT)
           defineVariable "mobileInt" (A.Mobile A.Int)
           defineFunction "function0" [A.Int] []
           defineFunction "function1" [A.Int] [("x", A.Int)]
@@ -60,6 +59,9 @@ startState
                                       [("x", A.Int), ("y", A.Int)]
   where
     ca = A.ChanAttributes False False
+    intsT = A.Array [A.UnknownDimension] A.Int
+    arrayLit = A.ArrayLiteral m []
+    chanIntT = A.Chan A.DirUnknown ca A.Int
 
 -- | Test the typechecker.
 testOccamTypes :: Test
@@ -186,6 +188,36 @@ testOccamTypes = TestList
     , testOK   254 $ A.AllocMobile m (A.Mobile twoIntsT) (Just twoIntsE)
     , testFail 255 $ A.AllocMobile m (A.Mobile unknownIntsT) (Just twoIntsE)
     , testFail 256 $ A.AllocMobile m (A.Mobile unknownIntsT) Nothing
+
+    -- Input items
+    , testOK   300 $ A.InCounted m intV intsV
+    , testFail 301 $ A.InCounted m realV intsV
+    , testFail 302 $ A.InCounted m intV intV
+    , testFail 303 $ A.InCounted m constIntV intsV
+    , testFail 304 $ A.InCounted m intV constIntsV
+    , testFail 305 $ A.InCounted m intV chansIntV
+    , testOK   306 $ A.InVariable m intV
+    , testFail 307 $ A.InVariable m constIntV
+    , testFail 308 $ A.InVariable m chanIntV
+
+    -- Output items
+    , testOK   310 $ A.OutCounted m intE twoIntsE
+    , testFail 311 $ A.OutCounted m realE twoIntsE
+    , testFail 312 $ A.OutCounted m intE intE
+    , testOK   313 $ A.OutExpression m intE
+    , testFail 313 $ A.OutExpression m chanIntE
+
+    -- Replicators
+    , testOK   320 $ A.For m i intE intE
+    , testFail 321 $ A.For m i realE intE
+    , testFail 322 $ A.For m i intE realE
+    , testOK   323 $ A.ForEach m i twoIntsE
+    , testOK   324 $ A.ForEach m i listE
+    , testFail 324 $ A.ForEach m i intE
+
+    -- Choices
+    , testOK   330 $ A.Choice m boolE skip
+    , testFail 331 $ A.Choice m intE skip
     ]
   where
     testOK :: (Show a, Data a) => Int -> a -> Test
@@ -200,13 +232,16 @@ testOccamTypes = TestList
                                         (OccamTypes.checkTypes orig)
                                         startState
 
-    intV = variable "someInt"
+    intV = variable "varInt"
     intE = intLiteral 42
+    realV = variable "varReal"
     realE = A.Literal m A.Real32 $ A.RealLiteral m "3.14159"
-    byteV = variable "someByte"
+    byteV = variable "varByte"
     byteE = byteLiteral 42
-    intsV = variable "someInts"
-    bytesV = variable "someBytes"
+    intsV = variable "varInts"
+    bytesV = variable "varBytes"
+    constIntV = variable "constInt"
+    constIntsV = variable "constInts"
     boolE = boolLiteral True
     unknownIntsT = A.Array [A.UnknownDimension] A.Int
     twoIntsT = A.Array [dimension 2] A.Int
@@ -227,6 +262,8 @@ testOccamTypes = TestList
     coord3T = A.Record (simpleName "COORD3")
     coord3 = A.RecordLiteral m [realE, realE, realE]
     chanIntV = variable "chanInt"
+    chanIntE = A.ExprVariable m chanIntV
+    chansIntV = variable "chanInt"
     mobileIntV = variable "mobileInt"
     sub0 = A.Subscript m A.NoCheck (intLiteral 0)
     sub0E = A.SubscriptedExpr m sub0
@@ -238,6 +275,8 @@ testOccamTypes = TestList
     function22 = simpleName "function22"
     listT = A.List A.Int
     listE = A.Literal m listT (A.ListLiteral m [intE, intE, intE])
+    i = simpleName "i"
+    skip = A.Skip m
 
 tests :: Test
 tests = TestLabel "OccamTypesTest" $ TestList