diff --git a/lab03/interp.lhs b/lab03/interp.lhs
new file mode 100644
index 0000000..5c6af06
--- /dev/null
+++ b/lab03/interp.lhs
@@ -0,0 +1,115 @@
+This File is _literate Haskell_.
+That means that (in some sense) code and comments are reversed.
+By default, everything that I type is actually a comment.
+To write code, I preface it with a 'greater than' symbol.
+
+In this lab, we will define a small language and its operational semantics.
+We'll first describe the language:
+
+e ::= true
+    | false
+    | if e then e else e
+
+The "::=" symbol above should be read as "can be", and "|" should be read as "or".
+The metavariable "e" represents an expression.
+Where needed, we will use "e1", "e2", "e'", etc. as additional metavariables
+for expressions.
+
+Representing this language in Haskell is fairly straightforward.
+(Note the use of the '>' to denote code below.)
+
+> data Exp = ETrue
+>          | EFalse
+>          | Eif Exp Exp Exp
+>  deriving Show
+
+
+We also need to decide what are the valid values in our language.
+The metavariable "v" stands for a value; again, we will use "v1", "v2", "v'", etc.
+as needed for clarity.
+For our initial language, only "true" and "false" will be valid values.
+Note that these are **also** valid expresisons in our language.
+
+v ::= true
+    | false
+
+As with our expressions, representing our values in Haskell is straightforward:
+
+> data Val = VTrue
+>          | VFalse
+>  deriving Show
+
+The next part is to define our "evaluate" function.
+We use a downarrow in the slides.
+Here we'll use a "->*".
+
+The first 2 rules define the evaluation of boolean expressions.
+The value "true" evaluates to itself, and the value "false"
+evaluates to itself.
+
+-------------
+true ->* true
+
+---------------
+false ->* false
+
+
+The next two rules define the behavior of our if expressions.
+Both rules specify that e1 should be evaluated first.
+Note that we say "evaluated to" and not "is".
+Saying "is" would imply "=", which might not be the case.
+
+If e1 evaluates to true, then e2 should be evaluated to get our result.
+The statements above the line are the "premises" or "preconditions"
+that must be true for this rule to apply.
+
+   e1 ->* true    e2 ->* v
+--------------------------------
+  if e1 then e2 else e3 ->* v
+
+If e1 evalates to false, then e3 should be evaluated to get our result.
+
+   e1 ->* false    e3 ->* v
+--------------------------------
+  if e1 then e2 else e3 ->* v
+
+
+With these rules defined, we can convert them to code.
+We represent "->*" with an "evaluate" function.
+Note that a "->*" in the premises should translate to a recursive call to evaluate.
+
+The VTrue case has been done for you.
+You must complete the other cases.
+
+
+> evaluate :: Exp -> Val
+> evaluate ETrue = VTrue
+> evaluate EFalse = error "TBD"
+> evaluate (Eif e1 e2 e3) = error "TBD"
+
+
+And here we have a couple of programs to test.
+prog1 should evaluate to VTrue and prog2 should evaluate to VFalse
+
+> prog1 = Eif ETrue ETrue EFalse
+> prog2 = Eif (Eif ETrue EFalse ETrue) ETrue (Eif ETrue EFalse ETrue)
+
+The following lines evaluate the test expressions and display the results.
+Note the type of main.  'IO ()' indicates that the function performs IO and returns nothing.
+The word 'do' begins a block of code, were you can effectively do sequential statements.
+(This is a crude generalization, but we'll talk more about what is going on in this function
+when we deal with the great and terrible subject of _monads_.)
+
+> main :: IO ()
+> main = do
+>   putStrLn $ "Evaluating '" ++ (show prog1) ++ "' results in " ++ (show $ evaluate prog1)
+>   putStrLn $ "Evaluating '" ++ (show prog2) ++ "' results in " ++ (show $ evaluate prog2)
+
+
+Once you have the evaluate function working
+you add in support the expressions 'succ e', 'pred e', and integers.
+With this change, it is possible for evaluate to get 'stuck',
+e.g. pred true.
+For a first pass, simply use the error function in these cases.
+
+
diff --git a/lab03/semantics.pdf b/lab03/semantics.pdf
new file mode 100644
index 0000000..2a32692
Binary files /dev/null and b/lab03/semantics.pdf differ
diff --git a/lab03/semantics.tex b/lab03/semantics.tex
new file mode 100644
index 0000000..9473ff2
--- /dev/null
+++ b/lab03/semantics.tex
@@ -0,0 +1,188 @@
+\documentclass{article}
+
+\usepackage{fullpage}
+%\usepackage{citesort}
+%\usepackage{url}
+%\usepackage{listings}
+\usepackage{color}
+
+
+% Commands for formatting figures
+\newcommand{\mydefhead}[2]{\multicolumn{2}{l}{{#1}}&\mbox{\emph{#2}}\\}
+\newcommand{\mydefcase}[2]{\qquad\qquad& #1 &\mbox{#2}\\}
+
+% Commands for language expressions and values
+\newcommand{\true}{\mbox{\tt true}}
+\newcommand{\false}{\mbox{\tt false}}\title{Operational Semantics for Bool* Language}
+\newcommand{\ife}[3]{\mbox{\tt if}~{#1}~\mbox{\tt then}~{#2}~\mbox{\tt else}~{#3}}
+\newcommand{\suc}[1]{\mbox{\tt succ}~{#1}}
+\newcommand{\prd}[1]{\mbox{\tt pred}~{#1}}
+
+% Big-step evaluation relation.
+% #1 is the expression.
+% #2 is the resulting value.
+\newcommand{\bstep}[2]{{#1} \Downarrow {#2}}
+
+% Command for formatting the name of the evaluation relation.
+\newcommand{\rel}[1]{ \mbox{\sc [#1]} }
+
+% Format for a big-step evaluation rule.
+% #1 is the name of the rule.
+% #2 are the premises.  Leave blank if there are none.
+% #3 is the conclusion.
+\newcommand{\bsrule}[3]{
+  \rel{#1} &
+  \frac{\strut\begin{array}{@{}c@{}} #2 \end{array}}
+       {\strut\begin{array}{@{}c@{}} #3 \end{array}}
+   \\~\\
+}
+
+\author{
+  Thomas H. Austin \\
+  San Jos\'{e} State University \\
+  thomas.austin@sjsu.edu
+  }
+
+\begin{document}
+\maketitle
+
+\begin{abstract}
+In this paper, we will provide a review of the big-step operational semantics
+for the Bool* language we discussed in class.
+\end{abstract}
+
+%%%%
+%\section{Introduction}
+
+Bool* is a very minimal language that allows us to experiment with operational semantics.
+
+First, we define the valid expressions in our language.
+These expressions dictate the possibilities of what expressions
+we may have in our source programs.
+(Note that other language might also have {\em statements}.
+Statements might not evaluate to a value;
+expressions always will.)
+
+\begin{figure}
+\caption{The Bool* language}
+\label{fig:lang}
+\[
+  \begin{array}{ll@{\qquad\qquad}l}
+  \mydefhead{e ::=\qquad\qquad\qquad\qquad}{Expressions}
+  \mydefcase{\true}{true value}
+  \mydefcase{\false}{false value}
+  \mydefcase{\ife e e e}{conditional expressions}
+  \\
+  \mydefhead{v ::=\qquad\qquad\qquad\qquad}{Values}
+  \mydefcase{\true}{true value}
+  \mydefcase{\false}{false value}
+\end{array}
+\]
+\end{figure}
+
+Figure~\ref{fig:lang} shows the list of expressions and values for the Bool* language.
+Expressions can be the value $\true$, the value $\false$,
+or the conditional expression $\ife e e e$.
+Note that conditional expressions have a recursive structure,
+with 3 sub-expressions.
+
+After evaluating a program, we should be able to produce a value in this language.
+(In other languages, we might hit a bad situation and need to crash instead;
+that won't happen in this language.)
+The valid values for Bool* are $\true$ and $\false$.
+
+With our expressions and values defined,
+we can now specify the semantics for our language.
+To do so, we will use the following big-step evaluation relation:
+
+\[
+  \bstep{e}{v}
+\]
+
+The above line should be read as ``the expression $e$ evaluates to the value $v$''.
+
+\begin{figure}
+\caption{Big-step semantics for Bool*}
+\label{fig:bigstep}
+  {\bf Evaluation Rules:~~~ \fbox{$\bstep{e}{v}$}} \\
+\[
+\begin{array}{r@{\qquad\qquad}c}
+\bsrule{B-Value}{}{
+  \bstep{v}{v}
+}
+\bsrule{B-IfTrue}{
+  \bstep{e_1}{\true} \\
+  \bstep{e_2}{v}
+}{
+  \bstep{\ife{e_1}{e_2}{e_3}}{v}
+}
+\bsrule{B-IfFalse}{
+  \bstep{e_1}{\false} \\
+  \bstep{e_3}{v}
+}{
+  \bstep{\ife{e_1}{e_2}{e_3}}{v}
+}
+\end{array}
+\]
+\end{figure}
+
+
+
+Figure~\ref{fig:bigstep} shows the big-step evaluation rules for the Bool* language.
+Of course, there are additional possible rules.
+
+The \rel{B-Value} rule applies when the expression (to the left of ``$\Downarrow$'')
+is also a value, as defined in Figure~\ref{fig:lang}.
+There are no premises for this rule (above the line),
+meaning that it is an {\em axiom}.
+This rule states that a value evaluates to itself,
+so that \true{} evaluates to \true{} and \false{} evaluates to \false{}.
+
+Two different rules are needed for handling conditional expressions.
+Which rule applies depends on the premises.
+
+For the \rel{B-IfTrue} rule,
+the premise states that $e_1$ evaluates to \true{}
+and $e_2$ evaluates to some value $v$.
+If the premise holds, then the result of evaluating the expression is the value $v$.
+The structure of \rel{B-IfFalse} is similar.
+
+
+\section*{Exercise}
+
+Let's extend the language with new features.
+Our new language will be called BoolInt*.
+The valid expressions and values are shown below:
+
+%\begin{figure}
+%\caption{The BoolInt* language}
+%\label{fig:lang2}
+\[
+  \begin{array}{ll@{\qquad\qquad}l}
+  \mydefhead{e ::=\qquad\qquad\qquad\qquad}{Expressions}
+  \mydefcase{\true}{true value}
+  \mydefcase{\false}{false value}
+  \mydefcase{i}{integers}
+  \mydefcase{\ife e e e}{conditional expressions}
+  \mydefcase{\suc e}{successor}
+  \mydefcase{\prd e}{predecessor}
+  \\
+  \mydefhead{v ::=\qquad\qquad\qquad\qquad}{Values}
+  \mydefcase{\true}{true value}
+  \mydefcase{\false}{false value}
+  \mydefcase{i}{integers}
+\end{array}
+\]
+%\end{figure}
+
+In addition to integers, our expanded language has the ability to increment an integer ($\suc e$)
+and decrement an integer ($\prd e$).
+
+Using LaTeX, write the evaluation rules for these additional constructs.
+If necessary, revise any existing rules.
+
+Then, add these new constructs to the Haskell interpreter that we have been working with.
+
+
+\end{document}
+