e ::= v | x | if e then e else e | e e
v ::= n | true | false | \x:t.e 
t ::= int | bool | t->t

Small-step operational semantics (selected rules):

(\x:t.e) e' --> e[x->e']	[beta reduction]

(Other ways to write this:

(\x:t.e) e' --> e[x/e']    e[e'\x]   e[x\e']   e[x\mapsto{}e']

 watch out for the direction of slashes!)

if true then e1 else e2 --> e1
if false then e1 else e2 --> e2

                    e0 --> e0'
------------------------------------------------
if e0 then e1 else e2 --> if e0' then e1 else e2

                    e1 --> e1'
------------------------------------------------
if e0 then e1 else e2 --> if e0 then e1' else e2

e2 --> e2'
-------------------------------
(\x:t.e1) e2 --> (\x:t.e1) e2'

e1 --> e1'
-------------------------------
(\x:t.e1) e2 --> (\x:t.e1') e2


Preservation:  G |- e:t  and e-->e'  then G |- e':t
Progress:      0 |- e:t  then either e\in v or 
                                     exists e' s.t. e-->e'

** = only possible reduction in call-by-value

**(\x.3) (if true then 0 else 1) --> (\x.3) 0 --> 3
(\x.3) (if true then 0 else 1) --> 3

**if true then ((\x.x) 3) else 1 --> (\x.x) 3 --> 3
if true then ((\x.x) 3) else 1 -->
  if true then 3 else 1 --> 3

=================================================

e ::= v | x | if e then e else e | e e
    | annot(Q,e) | check(Q,e)
v ::= (Q,n) | (Q,true) | (Q,false) | (Q,\x:t.e)
qt ::= (Q,int) | (Q,bool) | (Q,t->t)

Small-step operational semantics:

annot(Q,n) --> (Q,n)
(similar from other values)

         e --> e'
--------------------------
annot(Q,e) --> annot(Q,e')

(Q, \x:t.e) e' --> e[x->e']	[beta reduction]

if (Q, true) then e1 else e2 --> e1
if (Q, false) then e1 else e2 --> e2

check(Q, (Q',n)) --> (Q',n)      Q' <= Q
check(Q, (Q,true)) --> (Q,true)  Q' <= Q
...

    e --> e'
--------------------------
check(Q,e) --> check(Q,e')


Preservation:  G |- e:qt  and e --> e' then G |- e':qt
Progress:      0 |- e:qt  then either e\in v or 
                                     exists e' s.t. e-->e'


G |- e : qt   qt <= qt'
----------------------- [Sub]
    G |- e : qt'

With [Sub] integrated into the other rules:

Preservation:  G |- e:qt and e-->e' then G |- e':qt' qt'<=qt

==========================================================

Example for why Java < 1.5 wanted relaxed subtyping rules

int foo(Object[] a) {
  int sum = 0;
  for (int i = 0; i < a.length; i++)
    sum += a[i].hashCode();
  return sum;
}

List<String> <= List<Object>   ** false in Java 1.5

List<A> <= List<B>  requires A=B

G |- e : qt1   qt1 <= qt2
-------------------------
G |- e : qt2   qt2 <= qt3
-------------------------
G |- e : qt3

BECOMES

G |- e : qt1   qt1 <= qt3
-------------------------
G |- e : qt3


==========================================================

Integrating subtyping rule into application rule:

Step 1:  assume one use of subsumption before each hypothesis

G |- e1 : t1 -> t1'        G |- e2 : t2
t1 -> t1' <= t -> t'        t2 <= t
--------------------     --------------
G |- e1 : t -> t'         G |- e2 : t
--------------------------------------
          G |- e1 e2  : t'


Step 2: Erase -----'s and expand out <= for function types

G |- e1 : t1 -> t1'        G |- e2 : t2
t1' <= t'
t <= t1
t2 <= t
--------------------------------------
          G |- e1 e2  : t'

Step 3:  Erase intermediate type t, and since remaining
rules will assume some use of subsumption before each
hypothesis, remove subsumption on t1'

G |- e1 : t1 -> t1'   G |- e2 : t2   t2 <= t1
----------------------------------------------
          G |- e1 e2  : t1'