topical slide(s): creative technology / new media / game development(s)


  type stack T {
   $s : seq   T$ ;
  axioms:
   ${ true } push(t:T) { s' = s \. < > }$ 
   ${ s \neq << >> } pop() { s = { s' } \. < > }$ 
  };