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 <= List