Translation from basic While-language to $\lambda$-calculus Is there a simple way to translate programs written in a basic "While" language (such as Winskels Imp)?

I know about Church numerals and booleans, and I can see how if and while statements can be translated as

$$\mbox{if}~t_c~\mbox{then}~t_t~\mbox{else}~t_f\qquad\rightarrow\qquad(t_c t_t)t_f$$ and $$\mbox{while}~t_c~\mbox{do}~t_l \qquad\rightarrow\qquad \omega(\lambda r.(t_c (t_l; \omega r) I))$$ (with suitable definitions for $\omega$ and $I$).

Assignment however puzzles me.

One example translation of the following program

x := foo;
if x then t_1 else t_2


would be

$$(\lambda x.(x t_1)t_2)~foo$$

But I can't seem to find a general rule for it. How would for instance this program translate:

x := true;
y := false;
while x do
    x := y
Here is the toy language I am going to use. Note that locations are numbered. 

$$    A := n \quad | \quad x_k \quad | \quad A_1 + A_2 \quad | \quad  ... \text{ (where $n,k ∈ \mathbb{N})$ } $$
$$    B := A_1 = A_2 \quad | \quad  ...  $$ 
$$    C := \quad  C_1 ; C_2 \quad |\quad  x_k := A\quad  | \quad  skip \quad |\quad \mathop{if}~B~\mathop{then}~C_1~\mathop{else}~C_2 \quad | \quad  ...  $$

First, you have to encode states. 
What's a state ? It's map from your set $L$ of locations 
to your set $V$ of values. Here I choose to implement them
by a function $σ : \mathbb{N} → \mathbb{N}$. We'll call 
$Σ$ the set of states. 

There are two common operation over states : 
$$\mathop{get} : Σ → L → V$$
$$\mathop{get} = λs.λx.(s~x)$$

$$\mathop{set} : Σ → L → V → Σ$$
$$\mathop{set} = λs.λx.λv.\left(λk.\mathop{equal}~k~x~v~(s~k)\right)$$
where $equal$ is a λ-term representing equality between Church numerals. 

Then we have to encode arithmetical expressions as function from $Σ$ to $V$ 
$$⟦n⟧ = λs.\lceil n \rceil$$
$$⟦x_k⟧ = λs.get~s~\lceil k \rceil$$
$$⟦A_1 + A_2⟧ = λs.\mathop{plus}~(⟦A₁⟧~s)~(⟦A₂⟧~s)$$
$$\vdots$$
where $\mathop{plus}$ is a λ-term representing addition over Church numerals and 
$\lceil n \rceil$ is the $n$-th Church numeral. 

And boolean expressions as functions from $Σ$ to booleans: 
$$⟦A₁ = A₂⟧ = λs.\mathop{equal}~(⟦A₁⟧~s)~(⟦A₂⟧~s)$$
$$\vdots$$

Finally you encode your commands as "state transformers" from $Σ$ to $Σ$. 
$$ ⟦skip⟧ = λs.s $$
$$ ⟦x_k := A⟧ = λs.\mathop{set}~s~\lceil k \rceil~(⟦A⟧~s) $$
$$ ⟦C₁;C₂⟧ = ⟦C_2⟧ ∘ ⟦C_1⟧ = λs.⟦C_2⟧~(⟦C_1⟧~s)$$
$$ ⟦\mathop{if}~B~\mathop{then}~C_1~\mathop{else}~C_2⟧ = 
   λs.⟦B⟧~s~(⟦C₁⟧~s)~(⟦C₂⟧~s) $$
$$\vdots$$


Exercise 1: Prove the correctness of this compilation wrt to a standard operational semantics.  
Exercise 2: Check that everything works in a typed context (you will however need some kind of fixpoint operator to translate the while construction).