Thu Jul 16 14:35:00 CEST 2009

type checking vs. abstract interpretation

I would like to understand the connection between abstract evaluation
and type systems[1][2][3].  Damn.. LtU is always a good place to get

  "Conventional type-checking is big-step evaluation in the abstract:
   to find a type of an expression, we fully `evaluate' its immediate
   subterms to their types. Our paper[2] describes a different kind of
   type checking that is small-step evaluation in the abstract: it
   unzips an expression into a context and a redex."

[1] http://lambda-the-ultimate.org/node/2208
[2] http://okmij.org/ftp/Computation/#small-step-typechecking
[3] http://okmij.org/ftp/Computation/#teval