Typed Lambda-Calculus

Paul Levy (Birmingham)

This course is an introduction to the typed lambda-calculus, a language for describing functions and tuples, with sum, product and function types. We look at denotational semantics, using sets and functions, the substitution lemma and equational theory. We then explore some consequences of adding computational effects, under call- by-value and call-by-name evaluation.


Last modified: Fri Jan 10 16:12:41 GMT 2014