LARA

Type Soundness for Simply Typed Lambda Calculus

We apply the general method in Proving Safety Properties using Types to prove soundness of Simple Types for Lambda Calculus

Basic Notions

We consider the set of types $T$ given by these two rules:

  • int, bool $\in T$
  • if $t_1,t_2 \in T$, then also $(t_1 \to t_2) \in T$

(In particular types cannot have any 'variables' or 'parameters' as in more complex type systems.)

Examples of types: int, bool, int→bool, int→int, (int→bool)→bool, …

What is a configuration used to represent program execution?

What is the initial configuration?

What is the reduction relation $\leadsto$?

How to define the invariant $I$?

How can we define $error$?

  • such that $I$ implies $\lnot error$?
  • what kind of expressions will error denote?

Well Typed Programs Have no Immediate Errors

We show that $I$ implies $\lnot error$

Proof sketch:

Evaluation Preserve Types: Subject Reduction

We next show that the invariant $I$ is inductive

What does this mean?

Given $t_1$, can we guess what $t_2$ is?

What does $\leadsto$ mean by Operational Semantics of Lambda with Letrec if we exclude rules for let/letrec

  • primitive rule application in some context
    • $C[(plus\ \overline n_1\ \overline n_2)] \leadsto C[\overline{n_1+n_2}]$ where $\overline n$ denotes the constant $n$
    • $C[(ite\ true\ e_1\ e_2)] \leadsto C[e_1]$
    • $C[(ite\ false\ e_1\ e_2)] \leadsto C[e_2]$
  • beta reduction: $C[(\lambda x:t.e_1)\ e_2] \leadsto C[e_1[x:=e_2]]$

Subject Reduction for Plus

If

\begin{equation*}
   \Gamma \vdash C[(plus\ \overline{n_1}\ \overline{n_2})]:t
\end{equation*}

then

\begin{equation*}
   \Gamma \vdash C[(\overline{n_1+n_2})]:t
\end{equation*}

Proof sketch:

Subject Reduction for Ite

If

\begin{equation*}
   \Gamma \vdash C[(ite\ true\ e_1\ e_2)]:t
\end{equation*}

then

\begin{equation*}
   \Gamma \vdash C[e_1]:t
\end{equation*}

If

\begin{equation*}
   \Gamma \vdash C[(ite\ false\ e_1\ e_2)]:t
\end{equation*}

then

\begin{equation*}
   \Gamma \vdash C[e_2]:t
\end{equation*}

Proof sketch:

Subject Reduction for Beta Reduction Rule

If

\begin{equation*}
   \Gamma \vdash C[(\lambda x:t_1.e_1)\ e_2]:t
\end{equation*}

then

\begin{equation*}
   \Gamma \vdash  C[e_1[x:=e_2]]:t
\end{equation*}

Proof sketch:

Lemma: If $\Gamma \oplus \{ x \mapsto t_2 \} \vdash e_1:t_1$ and $\Gamma \vdash e_2 : t_2$, then $\Gamma \vdash e_1[x:=e_2]:t_1$.

Proof sketch:

Note on Variable Capture