Fri Sep 18 14:54:58 CEST 2009

Type Checking and Abstract Interpretation

When reading stuff in [2], I missed this[1] comment by Greg

  ``I'm toying with a interpreter/compiler for a Joy-like language,
    and of course the issue of typing came up. But instead of having
    static type inference or latent type checking, I've been
    interested in executing programs with types instead of values.''

Then moving on to the small-step abstract interpretation[4].

When dealing with (control) effects, small-step operational semantics
are easier to work with than coarser big-step / denotational
semantics, while the latter allow for syntax-directed techniques
(structural induction[5] over expressions).

[1] http://lambda-the-ultimate.org/node/834#comment-7658
[2] entry://20090716-143500
[3] http://kerneltrap.org/blog/6714
[4] http://okmij.org/ftp/papers/delim-control-logic.pdf
[5] http://en.wikipedia.org/wiki/Structural_induction