# 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.

Part 1: Concepts and Syntax

Part 2: Substitution and Equations

Part 3: From Pure to Effectful

Part 4: Denotational Semantics of Call-By-Value

Answers to Part 1's exercises, and further questions

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