Assignments are the only statements in an imperative programming
language responsible for changes on states. Consider any assignment
x:=t. It expects two arguments, a variable x of some type 
and an expression t which when evaluated in some environment yields
an expression of type . The expression t may of course refer
to some variable, but when we write something like x:=x+1, we mean
to evaluate the variable x in the current
environment and update x in this environment. Notice that the
environment is an implicit parameter to characterise the term in
assignments, which cannot be avoided if we mix pure expressions with
variables of the imperative programming language.
For an adequate encoding, we perform a functional abstraction and require the type of the second argument to explicitly mention the current environment i.e.,
assign:{sort|location->Type}
{x:location}((Env sort)->sort x)->prog|sort.
Boolean expressions in conditionals and loops may be represented similarly, yielding a many-sorted imperative programming language as an inductive type,
** Module lib_ipl Imports lib_locations
$prog : (location->Type)->Type(prog)
$skip : {sort|location->Type}prog|sort
$assign :
{sort|location->Type}{x:location}((Env sort)->sort x)->prog|sort
$seq : {sort|location->Type}(prog|sort)->(prog|sort)->prog|sort
$ifthenelse :
{sort|location->Type}((Env sort)->bool)->(prog|sort)->(prog|sort)->
prog|sort
$while :
{sort|location->Type}((Env sort)->bool)->(prog|sort)->prog|sort
$prog_elim :
{sort|location->Type}{C_prog:(prog|sort)->TYPE}
(C_prog (skip|sort))->
({x:location}{x8:(Env sort)->sort x}C_prog (assign x x8))->
({x6,x7:prog|sort}(C_prog x6)->(C_prog x7)->C_prog (seq x6 x7))->
({x3:(Env sort)->bool}{x4,x5:prog|sort}(C_prog x4)->(C_prog x5)->
C_prog (ifthenelse x3 x4 x5))->
({x1:(Env sort)->bool}{x2:prog|sort}(C_prog x2)->
C_prog (while x1 x2))->{z:prog|sort}C_prog z
[[sort|location->Type][C_prog:(prog|sort)->TYPE]
[f_skip:C_prog (skip|sort)]
[f_assign:{x:location}{x8:(Env sort)->sort x}C_prog (assign x x8)]
[f_seq:{x6,x7:prog|sort}(C_prog x6)->(C_prog x7)->C_prog (seq x6 x7)]
[f_ifthenelse:{x3:(Env sort)->bool}{x4,x5:prog|sort}(C_prog x4)->
(C_prog x5)->C_prog (ifthenelse x3 x4 x5)]
[f_while:{x1:(Env sort)->bool}{x2:prog|sort}(C_prog x2)->
C_prog (while x1 x2)][x:location][x8:(Env sort)->sort x]
[x6,x7:prog|sort][x3:(Env sort)->bool][x4,x5:prog|sort]
[x1:(Env sort)->bool][x2:prog|sort]
prog_elim C_prog f_skip f_assign f_seq f_ifthenelse f_while
(skip|sort) ==> f_skip
|| prog_elim C_prog f_skip f_assign f_seq f_ifthenelse f_while
(assign x x8) ==> f_assign x x8
|| prog_elim C_prog f_skip f_assign f_seq f_ifthenelse f_while
(seq x6 x7) ==>
f_seq x6 x7
(prog_elim C_prog f_skip f_assign f_seq f_ifthenelse f_while
x6)
(prog_elim C_prog f_skip f_assign f_seq f_ifthenelse f_while
x7)
|| prog_elim C_prog f_skip f_assign f_seq f_ifthenelse f_while
(ifthenelse x3 x4 x5) ==>
f_ifthenelse x3 x4 x5
(prog_elim C_prog f_skip f_assign f_seq f_ifthenelse
f_while x4)
(prog_elim C_prog f_skip f_assign f_seq f_ifthenelse
f_while x5)
|| prog_elim C_prog f_skip f_assign f_seq f_ifthenelse f_while
(while x1 x2) ==>
f_while x1 x2
(prog_elim C_prog f_skip f_assign f_seq f_ifthenelse f_while
x2)]
ifthen = ... :
{sort|location->Type}((Env sort)->bool)->(prog|sort)->prog|sort
limplies = ... :
{sort|location->Type}((Env sort)->Prop)->((Env sort)->Prop)->Prop
Assertion_or = ... :
{sort|location->Type}((Env sort)->Prop)->((Env sort)->Prop)->
(Env sort)->Prop
* limplies_refl = ... :
{sort|location->Type}{P:(Env sort)->Prop}limplies P P
* limplies_trans = ... :
{sort|location->Type}{P,Q,R:(Env sort)->Prop}(limplies P Q)->
(limplies Q R)->limplies P R