\documentclass{article} 

\usepackage{fullpage}
\usepackage{theorem}
\usepackage{ulem}
\usepackage{prooftree}

\usepackage{local}
\usepackage{code}

\newcommand{\finish}[1]{\marginpar{***}{\it [#1]}}

\newcommand{\B}{\ensuremath{\mathsf{B}}}
\renewcommand{\>}{\ensuremath{\rightarrow}}
\newcommand{\yields}{\ensuremath{\vdash}}

\theoremstyle{margin}
\theorembodyfont{\rmfamily}
\newtheorem{exercise}{Exercise}
\newtheorem{theorem}{Theorem}
\newtheorem{proof}{Proof}
\newtheorem{lemma}{Lemma}
\newtheorem{debriefing}[exercise]{Debriefing}
\newenvironment{solution}[1]
  {\begin{trivlist}\item[] {\bf \ref{#1}. }}
  {\end{trivlist}}

\begin{document}
\begin{center}
\fbox{\large\bf CIS 500 Software Foundations}\\[5pt]
{\large\bf Homework Assignment 6, }\\[5pt]
Simple Extensions of Simply-Typed Lambda Calculus \\[10pt]
{\bf Due:} Monday, November 1, 2004, by noon
\end{center}

\newcommand{\answer}[1]{
}

\noindent {\bf Submission instructions:} Same as last time.

\newcommand{\blank}{\ensuremath{\underline{\quad}}}
\newcommand{\true}{\ensuremath{\mathsf{true}}}
\newcommand{\false}{\ensuremath{\mathsf{false}}}
\newcommand{\conde}[3]{\ensuremath{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3}}
\newcommand{\by}[1]{\ensuremath{\using \textsc{[#1]}}}
\newcommand{\tvar}[3]{\ensuremath{\prooftree \justifies #1 \yields #2 : #3 \by{T-Var} \endprooftree}}
\newcommand{\goalpha}{\renewcommand{\theenumi}{\alph{enumi}}
\renewcommand{\labelenumi}{\textup{(\theenumi)}}}

\newcommand{\liti}{\ensuremath{<{l_i:T_i}^{i \in 1..n}>}}


\begin{exercise}
  Prove type safety for variants. You need to extend the following
  proofs with cases only for the rules in Figure 11-11. Also note that
  in this figure the value syntax for variants is missing. There is another
  form of values in the language and that form is \( <l = v> as\ T\). 
  
  \begin{enumerate}
    \item Extend the inversion lemma of the typing relation (9.3.1).
    \item Extend the canonical forms lemma (9.3.4).
    \item Extend the progress lemma (9.3.5).
    \item Extend the substitution lemma (9.3.8). As this lemma is stated
      in the textbook, it must be proved by induction on the {\em
        depth} of the typing derivation.  Also to prove this lemma,
      you need to extend the definition for substitution within
      variants.  You may assume that the permutation and weakening
      lemmas hold for the lambda calculus extended with variants.
    \item Extend the preservation theorem (9.3.9).

  \end{enumerate}

\end{exercise}


\begin{exercise}
In O'Caml, we can write the following program:

\begin{verbatim}
let rec take (l : bool list) : bool list = 
  match l with 
    [] -> []
  | hd::tl -> hd :: skip tl
and skip (l : bool list) : bool list = 
  match l with 
    [] -> [] 
  | hd::tl -> take tl
in
  take [true,false,true]
\end{verbatim}

How would you write this program in the language of Chapter 11?
\end{exercise}


\begin{exercise}
TAPL 11.12.2
\end{exercise}

\answer{ }

\begin{debriefing}
\item \begin{enumerate}
\item How many hours (per person) did you spend on this assignment?
\item Would you rate it as easy, moderate, or difficult?
\item Did everyone in your study group participate?
\item How deeply do you feel you understand the material it covers
(0\%--100\%)? 
\end{enumerate}

\item If you have any other comments, we would like to hear them;
  please send them to {\tt cis500@cis.upenn.edu}.
\end{debriefing}
\end{document}


