It can be argued that the development and study of high-level programming languages is a central task for computer science research, and enormous progress has indeed been made from the machine-level coding of the 40s to today's functional and object-oriented languages. In this module, we will study the features that have emerged as recurring themes in high-level languages, though they are expressed in a variety of ways. We will use the lambda calculus as a meta language to express theses features concretely and precisely. At this level of abstraction, 'computation' becomes 'evaluation' of expressions, rather than the execution of machine instructions. We will look at ways to specify this process in a precise fashion and thus discover some key design decisions that have to be made when developing a concrete language. Types can be used to constrain the range of valid programs and thus help the programmer to develop well-structured code. We will see how polymorphism and subtyping extend the expressivity of simple type disciplines without sacrificing semantics.