diff --git a/asllib/doc/ASLTypingReference.tex b/asllib/doc/ASLTypingReference.tex
index a18687c22a..1717177bae 100644
--- a/asllib/doc/ASLTypingReference.tex
+++ b/asllib/doc/ASLTypingReference.tex
@@ -2136,6 +2136,370 @@ \subsection{Comments}
   \identr{TTGQ}, \identi{YHML}, \identi{YHRP}, \identi{VMZF}, \identi{YXSY},
   \identi{LGHJ}, \identi{RXLG}.
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\chapter{Typing of types}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a
+rewritten type~\texttt{new\_ty} and one of the following applies:
+\begin{itemize}
+  \item TypingRule.TString (see Section~\ref{sec:TypingRule.TString});
+  \item TypingRule.TReal (see Section~\ref{sec:TypingRule.TReal});
+  \item TypingRule.TBool (see Section~\ref{sec:TypingRule.TBool});
+  \item TypingRule.TNamed (see Section~\ref{sec:TypingRule.TNamed});
+  \item TypingRule.TInt (see Section~\ref{sec:TypingRule.TInt});
+  \item TypingRule.TBits (see Section~\ref{sec:TypingRule.TBits});
+  \item TypingRule.TTuple (see Section~\ref{sec:TypingRule.TTuple});
+  \item TypingRule.TArray (see Section~\ref{sec:TypingRule.TArray});
+  \item TypingRule.TEnumDecl (see Section~\ref{sec:TypingRule.TEnumDecl});
+  \item TypingRule.TRecordExceptionDecl (see
+    Section~\ref{sec:TypingRule.TRecordExceptionDecl});
+  \item TypingRule.TNonDecl (see Section~\ref{sec:TypingRule.TNonDecl});
+  \item TypingRule.TBitField (see Section~\ref{sec:TypingRule.TBitField}).
+\end{itemize}
+
+
+\section{TypingRule.TString \label{sec:TypingRule.TString}}
+
+\subsection{Prose}
+Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a
+rewritten type~\texttt{new\_ty} and all of the following apply:
+\begin{itemize}
+  \item \texttt{ty} is the string type \TString.
+  \item \texttt{new\_ty} is the string type \TString.
+\end{itemize}
+
+\subsection{Example}
+In the following example, all the uses of \texttt{string} are valid:
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TString.asl}
+
+\subsection{Code}
+\VerbatimInput[firstline=\TStringBegin, lastline=\TStringEnd]{../Typing.ml}
+
+
+\isempty{\subsection{Comments}}
+
+\section{TypingRule.TReal \label{sec:TypingRule.TReal}}
+
+\subsection{Prose}
+Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a
+rewritten type~\texttt{new\_ty} and all of the following apply:
+\begin{itemize}
+  \item \texttt{ty} is the real type \TReal.
+  \item \texttt{new\_ty} is the real type \TReal.
+\end{itemize}
+
+
+\subsection{Example}
+In the following example, all the uses of \texttt{real} are valid:
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TReal.asl}
+
+
+\subsection{Code}
+\VerbatimInput[firstline=\TRealBegin, lastline=\TRealEnd]{../Typing.ml}
+
+
+\isempty{\subsection{Comments}}
+
+
+\section{TypingRule.TBool \label{sec:TypingRule.TBool}}
+
+\subsection{Prose}
+Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a
+rewritten type~\texttt{new\_ty} and all of the following apply:
+\begin{itemize}
+  \item \texttt{ty} is the boolean type;
+  \item \texttt{new\_ty} is the boolean type.
+\end{itemize}
+
+\subsection{Example}
+In the following example, all the uses of \texttt{boolean} are valid:
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TBool.asl}
+
+\subsection{Code}
+\VerbatimInput[firstline=\TBoolBegin, lastline=\TBoolEnd]{../Typing.ml}
+
+
+\isempty{\subsection{Comments}}
+
+
+\section{TypingRule.TNamed \label{sec:TypingRule.TNamed}}
+
+\subsection{Prose}
+Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a
+rewritten type~\texttt{new\_ty} and all of the following apply:
+\begin{itemize}
+  \item \texttt{ty} is the a named type \texttt{x};
+  \item One of the following applies:
+    \begin{itemize}
+      \item \texttt{x} is bound in \texttt{tenv} to a type;
+      \item an error ``\texttt{Undefined Identifier}'' is raised.
+    \end{itemize}
+  \item \texttt{new\_ty} is \texttt{ty}.
+\end{itemize}
+
+\subsection{Example}
+In the following example, all the uses of \texttt{MyType} are valid:
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TNamed.asl}
+
+\subsection{Code}
+\VerbatimInput[firstline=\TNamedBegin, lastline=\TNamedEnd]{../Typing.ml}
+
+
+\isempty{\subsection{Comments}}
+
+
+\section{TypingRule.TInt \label{sec:TypingRule.TInt}}
+
+\subsection{Prose}
+Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a
+rewritten type~\texttt{new\_ty} and one of the following applies:
+\begin{itemize}
+  \item All of the following apply:
+    \begin{itemize}
+      \item \texttt{ty} is the unconstrained integer type;
+      \item \texttt{new\_ty} is the unconstrained integer type.
+    \end{itemize}
+  \item All of the following apply:
+    \begin{itemize}
+      \item \texttt{ty} is a under-constrained integer type;
+      \item \texttt{new\_ty} is the under-constrained integer type \texttt{ty}.
+    \end{itemize}
+  \item All of the following apply:
+    \begin{itemize}
+      \item \texttt{ty} is the well-constrained integer type constrained by
+        \texttt{constraints};
+      \item \texttt{constraints'} is the result of annotating each of the
+        constraints in \texttt{constraints};
+      \item \texttt{new\_ty} is the well-constrained integer type constrained
+        by \texttt{constraints}.
+    \end{itemize}
+\end{itemize}
+
+\subsection{Example}
+
+In the following examples, all the uses of integer types are valid:
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TIntUnConstrained.asl}
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TIntWellConstrained.asl}
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TIntUnderConstrained.asl}
+
+\subsection{Code}
+\VerbatimInput[firstline=\TIntBegin, lastline=\TIntEnd]{../Typing.ml}
+
+\isempty{\subsection{Comments}}
+
+
+\section{TypingRule.TBits \label{sec:TypingRule.TBits}}
+
+\subsection{Prose}
+Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a
+rewritten type~\texttt{new\_ty} and all of the following apply:
+\begin{itemize}
+  \item \texttt{ty} is the bit-vector type with width given by the expression
+    \texttt{e\_width} and the bitfields given by \texttt{bitfields};
+  \item \texttt{e\_width'} is the result of annotating the statically-evaluable integer expression \texttt{e\_width};
+  \item \texttt{bitfields'} is the result of annotating the bitfields \texttt{bitfields}
+  \item \texttt{new\_ty} is the bit-vector type with width given by the expression
+    \texttt{e\_width'} and the bitfields given by \texttt{bitfields'};
+\end{itemize}
+
+\subsection{Example}
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TBits.asl}
+
+
+\subsection{Code}
+In the following example, all the uses of bitvector types are valid:
+\VerbatimInput[firstline=\TBitsBegin, lastline=\TBitsEnd]{../Typing.ml}
+
+
+\isempty{\subsection{Comments}}
+
+
+\section{TypingRule.TTuple \label{sec:TypingRule.TTuple}}
+
+\subsection{Prose}
+Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a
+rewritten type~\texttt{new\_ty} and all of the following apply:
+\begin{itemize}
+  \item \texttt{ty} is the tuple type with member types \texttt{tys};
+  \item \texttt{tys'} is the result of annotating all the types in
+    \texttt{tys};
+  \item \texttt{new\_ty} is the tuple type with member types \texttt{tys'}.
+\end{itemize}
+
+\subsection{Example}
+In the following example, all the uses of tuple types are valid:
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TTuple.asl}
+
+
+\subsection{Code}
+\VerbatimInput[firstline=\TTupleBegin, lastline=\TTupleEnd]{../Typing.ml}
+
+
+\isempty{\subsection{Comments}}
+
+
+\section{TypingRule.TArray \label{sec:TypingRule.TArray}}
+
+\subsection{Prose}
+Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a
+rewritten type~\texttt{new\_ty} and all of the following apply:
+\begin{itemize}
+  \item All of the following holds:
+    \begin{itemize}
+      \item \texttt{ty} is the array type indexed by integer bounded by the
+        expression \texttt{e} and of elements of type \texttt{t};
+      \item \texttt{t'} is the result of annotating the type \texttt{t} in
+        environment \texttt{env};
+      \item \texttt{e'} is the result of annotating the statically evaluable
+        integer expression \texttt{e};
+      \item \texttt{new\_ty} is the array type indexed by integer bounded by
+        the expression \texttt{e'} and of elements of type \texttt{t'};
+    \end{itemize}
+  \item All of the following holds:
+    \begin{itemize}
+      \item \texttt{ty} is the array type indexed by an enumeration type named
+        \texttt{s} and of elements of type \texttt{t};
+      \item \texttt{s} is bound in \texttt{env} to an enumeration type;
+      \item \texttt{t'} is the result of annotating the type \texttt{t} in
+        environment \texttt{env};
+      \item \texttt{new\_ty} is the array type indexed by an enumeration type
+        named \texttt{s} and of elements of type \texttt{t'};
+    \end{itemize}
+\end{itemize}
+
+\subsection{Example}
+In the following example, all the uses of array types are valid:
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TArray.asl}
+
+\subsection{Code}
+\VerbatimInput[firstline=\TArrayBegin, lastline=\TArrayEnd]{../Typing.ml}
+
+
+\isempty{\subsection{Comments}}
+
+
+\section{TypingRule.TEnumDecl \label{sec:TypingRule.TEnumDecl}}
+
+\subsection{Prose}
+Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a
+rewritten type~\texttt{new\_ty} and all of the following apply:
+\begin{itemize}
+  \item \texttt{ty} is the enumeration type with enumeration literals
+    \texttt{li};
+  \item This is the declaration of \texttt{ty};
+  \item One of the following applies:
+    \begin{itemize}
+      \item \texttt{li} does not contains any duplicate enumeration literal.
+      \item an error ``\texttt{Already declared identifier}'' is raised;
+    \end{itemize}
+  \item \texttt{new\_ty} is the enumeration type \texttt{ty}.
+\end{itemize}
+
+\subsection{Example}
+In the following example, all the uses of enumeration types are valid:
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TEnumDecl.asl}
+
+
+\subsection{Code}
+\VerbatimInput[firstline=\TEnumDeclBegin, lastline=\TEnumDeclEnd]{../Typing.ml}
+
+
+\isempty{\subsection{Comments}}
+
+
+\section{TypingRule.TRecordExceptionDecl \label{sec:TypingRule.TRecordExceptionDecl}}
+
+\subsection{Prose}
+Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a
+rewritten type~\texttt{new\_ty} and one of the following applies:
+\begin{itemize}
+  \item All of the following apply:
+    \begin{itemize}
+      \item \texttt{ty} is the record type with fields \texttt{fields};
+      \item This is the declaration of \texttt{ty};
+      \item One of the following applies:
+        \begin{itemize}
+          \item \texttt{fields} does not contains any duplicate field.
+          \item an error ``\texttt{Already declared identifier}'' is raised;
+        \end{itemize}
+      \item \texttt{fields'} is the result of annotating each type in
+        \texttt{fields};
+      \item \texttt{new\_ty} is the record type with fields \texttt{fields'};
+    \end{itemize}
+  \item All of the following apply:
+    \begin{itemize}
+      \item \texttt{ty} is the exception type with fields \texttt{fields};
+      \item This is the declaration of \texttt{ty};
+      \item One of the following applies:
+        \begin{itemize}
+          \item \texttt{fields} does not contains any duplicate field.
+          \item an error ``\texttt{Already declared identifier}'' is raised;
+        \end{itemize}
+      \item \texttt{fields'} is the result of annotating each type in
+        \texttt{fields};
+      \item \texttt{new\_ty} is the exception type with fields \texttt{fields'};
+    \end{itemize}
+\end{itemize}
+
+
+\subsection{Example}
+In the following example, all the uses of record or exception types are valid:
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TRecordExceptionDecl.asl}
+
+
+\subsection{Code}
+\VerbatimInput[firstline=\TRecordExceptionDeclBegin, lastline=\TRecordExceptionDeclEnd]{../Typing.ml}
+
+
+\isempty{\subsection{Comments}}
+
+
+\section{TypingRule.TNonDecl \label{sec:TypingRule.TNonDecl}}
+
+\subsection{Prose}
+Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a
+rewritten type~\texttt{new\_ty} and all of the following apply:
+\begin{itemize}
+  \item One of the following applies:
+    \begin{itemize}
+      \item \texttt{ty} is a record type;
+      \item \texttt{ty} is an exception type;
+      \item \texttt{ty} is an enumeration type;
+    \end{itemize}
+  \item This is not the declaration of \texttt{ty};
+  \item An error ``Cannot use anonymous form of enumerations, record, or exceptions here.'' is raised.
+\end{itemize}
+
+\subsection{Example}
+
+In the following example, the use of a record type out of a declaration is invalid:
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TNonDecl.asl}
+
+\subsection{Code}
+\VerbatimInput[firstline=\TNonDeclBegin, lastline=\TNonDeclEnd]{../Typing.ml}
+
+
+\isempty{\subsection{Comments}}
+
+
+\section{TypingRule.TBitField \label{sec:TypingRule.TBitField}}
+
+\subsection{Prose}
+
+
+\subsection{Example}
+In the following example, all the uses of bitvector types with bitfields are valid:
+\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TBitField.asl}
+
+
+\subsection{Code}
+\VerbatimInput[firstline=\TBitFieldBegin, lastline=\TBitFieldEnd]{../Typing.ml}
+
+
+\isempty{\subsection{Comments}}
+
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \chapter{Typing of Expressions}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/asllib/instrumentation.ml b/asllib/instrumentation.ml
index c986ea7869..9ce9546182 100644
--- a/asllib/instrumentation.ml
+++ b/asllib/instrumentation.ml
@@ -428,6 +428,18 @@ module TypingRule = struct
     | DeclareGlobalStorage
     | DeclareTypeDecl
     | Specification
+    | TString
+    | TReal
+    | TBool
+    | TNamed
+    | TInt
+    | TBits
+    | TTuple
+    | TArray
+    | TEnumDecl
+    | TRecordExceptionDecl
+    | TNonDecl
+    | TBitField
 
   let to_string : t -> string = function
     | BuiltinSingularType -> "BuiltinSingularType"
@@ -561,6 +573,18 @@ module TypingRule = struct
     | DeclareGlobalStorage -> "DeclareGlobalStorage"
     | DeclareTypeDecl -> "DeclareTypeDecl"
     | Specification -> "Specification"
+    | TString -> "TString"
+    | TReal -> "TReal"
+    | TBool -> "TBool"
+    | TNamed -> "TNamed"
+    | TInt -> "TInt"
+    | TBits -> "TBits"
+    | TTuple -> "TTuple"
+    | TArray -> "TArray"
+    | TEnumDecl -> "TEnumDecl"
+    | TRecordExceptionDecl -> "TRecordExceptionDecl"
+    | TNonDecl -> "TNonDecl"
+    | TBitField -> "TBitField"
 
   let pp f r = to_string r |> Format.pp_print_string f
 
@@ -674,6 +698,18 @@ module TypingRule = struct
       CatcherNone;
       CatcherSome;
       Subprogram;
+      TString;
+      TReal;
+      TBool;
+      TNamed;
+      TInt;
+      TBits;
+      TTuple;
+      TArray;
+      TEnumDecl;
+      TRecordExceptionDecl;
+      TNonDecl;
+      TBitField;
     ]
 
   let all_nb = List.length all
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TArray.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TArray.asl
new file mode 100644
index 0000000000..a8f9271c89
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TArray.asl
@@ -0,0 +1,22 @@
+type MyType of array [4] of integer;
+
+func foo (x: array [4] of integer) => array [4] of integer
+begin
+  var y = x;
+  y[3] = 2;
+  return y;
+end
+
+func main () => integer
+begin
+  var x: array [4] of integer;
+
+  x[1] = 1;
+  print(x);
+  x = foo (x as array [4] of integer);
+  
+  let y: array [4] of integer = x;
+
+
+  return 0;
+end
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TBitField.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TBitField.asl
new file mode 100644
index 0000000000..fa2ad33fb2
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TBitField.asl
@@ -0,0 +1,20 @@
+type MyType of bits(4) { [3:2] A, [1] B };
+
+func foo (x: bits(4) { [3:2] A, [1] B }) => bits(4) { [3:2] A, [1] B }
+begin
+  return x;
+end
+
+func main () => integer
+begin
+  var x: bits(4) { [3:2] A, [1] B };
+
+  x = '1010';
+  x = foo (x as bits(4) { [3:2] A, [1] B });
+  
+  let y: bits(4) { [3:2] A, [1] B } = x;
+
+  assert x as bits(4) { [3:2] A, [1] B } == x;
+
+  return 0;
+end
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TBits.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TBits.asl
new file mode 100644
index 0000000000..957841ceb9
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TBits.asl
@@ -0,0 +1,21 @@
+type MyType of bits(4);
+
+func foo (x: bits(4)) => bits(4)
+begin
+  return NOT x;
+end
+
+func main () => integer
+begin
+  var x: bits(4);
+
+  x = '1010';
+  x = foo (x as bits(4));
+  
+  let y: bits(4) = x;
+
+  assert x as bits(4) == x;
+
+  return 0;
+end
+
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TBool.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TBool.asl
new file mode 100644
index 0000000000..4614a18666
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TBool.asl
@@ -0,0 +1,20 @@
+type MyType of boolean;
+
+func foo (x: boolean) => boolean
+begin
+  return FALSE --> x;
+end
+
+func main () => integer
+begin
+  var x: boolean;
+
+  x = TRUE;
+  x = foo (x as boolean);
+  
+  let y: boolean = x && x;
+
+  assert x as boolean == x;
+
+  return 0;
+end
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TEnumDecl.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TEnumDecl.asl
new file mode 100644
index 0000000000..37ea57e9b1
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TEnumDecl.asl
@@ -0,0 +1,5 @@
+type MyEnum of enumeration { A, B, C };
+
+func main () => integer
+begin return 0; end
+
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TIntUnConstrained.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TIntUnConstrained.asl
new file mode 100644
index 0000000000..653fbd8b3e
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TIntUnConstrained.asl
@@ -0,0 +1,20 @@
+type MyType of integer; 
+func foo (x: integer) => integer
+begin
+  return x;
+end
+
+func main () => integer
+begin
+  var x: integer;
+
+  x = 4;
+  x = foo (x as integer);
+  
+  let y: integer = x;
+
+  assert x as integer == x;
+
+  return 0;
+end
+
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TIntUnderConstrained.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TIntUnderConstrained.asl
new file mode 100644
index 0000000000..d9f840573b
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TIntUnderConstrained.asl
@@ -0,0 +1,18 @@
+func foo {N} (x: bits(N)) => integer
+begin
+  return N;
+end
+
+func bar (N: integer) => bits(N)
+begin
+  return Zeros(N);
+end
+
+func main() => integer
+begin
+  assert 3 == foo ('101');
+  assert bar(3) == '000';
+
+  return 0;
+end
+
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TIntWellConstrained.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TIntWellConstrained.asl
new file mode 100644
index 0000000000..128bd653fe
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TIntWellConstrained.asl
@@ -0,0 +1,21 @@
+type MyType of integer {1..12};
+
+func foo (x: integer {1..12}) => integer {1..12}
+begin
+  return x;
+end
+
+func main () => integer
+begin
+  var x: integer {1..12};
+
+  x = 4;
+  x = foo (x as integer {1..12});
+  
+  let y: integer {1..12} = x;
+
+  assert x as integer {1..11} == x;
+
+  return 0;
+end
+
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TNamed.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TNamed.asl
new file mode 100644
index 0000000000..14e25098d7
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TNamed.asl
@@ -0,0 +1,21 @@
+type MyType of integer;
+
+func foo (x: MyType) => MyType
+begin
+  return x;
+end
+
+func main () => integer
+begin
+  var x: MyType;
+
+  x = 4;
+  x = foo (x as MyType);
+  
+  let y: MyType = x;
+
+  assert x as MyType == x;
+
+  return 0;
+end
+
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TNonDecl.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TNonDecl.asl
new file mode 100644
index 0000000000..ac7dde2aa4
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TNonDecl.asl
@@ -0,0 +1,2 @@
+func (x: record { a: integer, b: boolean }) => integer
+begin return 0; end
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TReal.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TReal.asl
new file mode 100644
index 0000000000..5a1804232c
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TReal.asl
@@ -0,0 +1,21 @@
+type MyType of real;
+
+func foo (x: real) => real
+begin
+  return x + 1.0;
+end
+
+func main () => integer
+begin
+  var x: real;
+
+  x = 3.141592;
+  x = foo (x as real);
+  
+  let y: real = x + x;
+
+  assert x as real == x;
+
+  return 0;
+end
+
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TRecordExceptionDecl.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TRecordExceptionDecl.asl
new file mode 100644
index 0000000000..33e05e5fed
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TRecordExceptionDecl.asl
@@ -0,0 +1,6 @@
+type MyRecord of record { a: integer, b: boolean };
+type MyException of exception { a: integer, b: boolean };
+
+func main () => integer
+begin return 0; end
+
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TString.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TString.asl
new file mode 100644
index 0000000000..9ad08a6e16
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TString.asl
@@ -0,0 +1,20 @@
+type MyType of string;
+
+func foo (x: string) => string
+begin
+  return x;
+end
+
+func main () => integer
+begin
+  var x: string;
+
+  x = "foo";
+  x = foo (x as string);
+  
+  let y: string = x;
+
+  assert x as string == x;
+
+  return 0;
+end
diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TTuple.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TTuple.asl
new file mode 100644
index 0000000000..cc16ee3b76
--- /dev/null
+++ b/asllib/tests/ASLTypingReference.t/TypingRule.TTuple.asl
@@ -0,0 +1,22 @@
+type MyType of (integer, boolean);
+
+func foo (x: (integer, boolean)) => (integer, boolean)
+begin
+  let (z, y): (integer, boolean) = x;
+  return (z + 1, FALSE --> y);
+end
+
+func main () => integer
+begin
+  var x: (integer, boolean);
+
+  x = (3, TRUE);
+  x = foo (x as (integer, boolean));
+  
+  let y: (integer, boolean) = x;
+
+  let (x0, x1) = x as (integer, boolean);
+  assert x0 == 4 && x1 == TRUE;
+
+  return 0;
+end
diff --git a/asllib/tests/ASLTypingReference.t/run.t b/asllib/tests/ASLTypingReference.t/run.t
index 120ee3feff..ee2db85f1c 100644
--- a/asllib/tests/ASLTypingReference.t/run.t
+++ b/asllib/tests/ASLTypingReference.t/run.t
@@ -21,3 +21,22 @@ ASL Typing Reference:
   $ aslref TypingRule.LDTyped.asl
   $ aslref TypingRule.LDTuple.asl
   $ aslref TypingRule.Lit.asl
+
+ASL Typing Reference / annotating types:
+  $ aslref TypingRule.TReal.asl
+  $ aslref TypingRule.TBool.asl
+  $ aslref TypingRule.TNamed.asl
+  $ aslref TypingRule.TIntUnConstrained.asl
+  $ aslref TypingRule.TIntWellConstrained.asl
+  $ aslref TypingRule.TIntUnderConstrained.asl
+  $ aslref TypingRule.TBits.asl
+  $ aslref TypingRule.TTuple.asl
+  $ aslref TypingRule.TArray.asl
+  [0, 1, 0, 0]
+  $ aslref TypingRule.TEnumDecl.asl
+  $ aslref TypingRule.TRecordExceptionDecl.asl
+  $ aslref TypingRule.TNonDecl.asl
+  File TypingRule.TNonDecl.asl, line 1, characters 5 to 6:
+  ASL Error: Cannot parse.
+  [1]
+  $ aslref TypingRule.TBitField.asl