Untyped (nominal) lambda-calculus with integers and the conditional

http://okmij.org/ftp/Computation/Computation.html#teval

- The Abstract of the lecture notes
- We expound a view of type checking as evaluation with `abstract values'. Whereas dynamic semantics, evaluation, deals with (dynamic) values like 0, 1, etc., static semantics, type checking, deals with approximations like int. A type system is sound if it correctly approximates the dynamic behavior and predicts its outcome: if the static semantics predicts that a term has the type int, the dynamic evaluation of the term, if it terminates, will yield an integer.

As object language, we use simply-typed and let-polymorphic lambda calculi with integers and integer operations as constants. We use Haskell as a metalanguage in which to write evaluators, type checkers, type reconstructors and inferencers for the object language.

We explore the deep relation between parametric polymorphism and `inlining`

. Polymorphic type
checking then is an optimization allowing us to type check a polymorphic term at the place of its
definition rather than at the places of its use.

Joint work with Chung-chieh Shan.

Version The current version is 1.1, July 2008. References lecture.pdf [199K]