\documentclass{article} 

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

\newcommand{\B}{\ensuremath{\mathsf{B}}}
\renewcommand{\>}{\ensuremath{\rightarrow}}
\newcommand{\yields}{\ensuremath{\vdash}}
\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)}}}

\theoremstyle{margin}
\theorembodyfont{\rmfamily}
\newtheorem{exercise}{Exercise}
\newtheorem{theorem}{Theorem}
\newtheorem{proof}{Proof}
\newtheorem{lemma}{Lemma}
\newtheorem{debriefing}[exercise]{Debriefing}

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

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

\begin{exercise}
TAPL 9.2.1
\end{exercise}

\begin{exercise} 
  The following derivation trees of typing judgements in the simply
  typed $\lambda$-calculus with booleans are incomplete. If possible,
  fill in the missing types (marked with a $\blank$) and complete the
  derivation tree. For terms that are not typable, prove it.

{
\goalpha
\begin{enumerate}
\item{
$\prooftree
\justifies
\emptyset \yields \lambda x : \B . \lambda y : (\B \> \B) . y\ x : \blank
\by{T-???}
\endprooftree
$}

\item{$\prooftree
\justifies
\emptyset \yields (\lambda x : \blank . x\ x)\ (\lambda x : \blank . x\ x) : \blank
\by{T-???}
\endprooftree$}

\item{$\prooftree
\justifies
{ x : \B \> \B \yields (\lambda x : \B . x) : \blank}
\by{T-???}
\endprooftree$}

\item {$\prooftree
\justifies
  x : \B \> \B \yields (\lambda y : \B . x) : \blank
\by{T-???}
\endprooftree$}

\item{$\prooftree
\justifies
  g : \B \> \B \yields \lambda y : \B . g\ (\conde{y}{\false}{y}) : \blank \> \blank
\by{T-???}
\endprooftree$}


\item{$
\prooftree
\justifies
\emptyset \yields 
    \lambda x : \blank . 
    \lambda y : \blank . 
    x\ (\lambda f : \B \> \B . f\ y) : \blank \> \blank \> \B
\by{T-???}
\endprooftree$}

\end{enumerate}
}
\end{exercise}

\begin{exercise}
TAPL 9.3.10
\end{exercise}

\begin{exercise}

  Recall the definition of the simply typed $\lambda$-calculus with
  pairs (see TAPL, Figure 11-5).

{ \goalpha
\begin{enumerate}
\item State and prove the substitution lemma. (N.B., you only have to
write down the cases that change when we add pairs.)

\item Prove the preservation theorem for the same system. You may use
  any other lemmas (inversion, weakening, etc.) that you need without
  proof, but you must give their statements.

\end{enumerate}
}
\end{exercise}

\begin{exercise}
Prove part (1) of Theorem 9.5.2 in TAPL. 
\end{exercise}

\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}