In the previous part of the book we have introduced and studied an imperative language called IMP. In this chapter we move our attention to functional languages. In particular, we introduce HOFL, a simple higher-order functional language that allows for the explicit construction of infinitely many types. We overview Church and Curry type theories. Then, we present a lazy operational semantics, which corresponds to a call-by-name strategy, namely actual parameters are passed to functions without evaluating them. This view is contrasted with the eager evaluation semantics, which corresponds to a call-by-value strategy, where all actual parameters are evaluated before being passed to functions. The operational semantics evaluates (well-typed) terms to suitable canonical forms.