# Conclusion

That’s the end! In this course, we learned about

**Functions**, as embodied in the λ-calculus. This single concept is powerful enough to express any computation a Turing machine can, so learning how to define the operational semantics of functions is a fast-track to learning how to define the operational semantics of a full programming language.

**Types**: We learned how to define type systems, which enable us to prove some static guarantees about a program’s behavior (type safety or “well-typed programs don’t get stuck”). But our first attempt was also unduly restrictive; we looked at several ways of increasing expressivity, in both the mathematical sense (is it Turing complete?) and practical sense (would you want to program in this?).

**Effects**: Whether untyped or typed, we actually can’t express everything we want to, if we use the stricter notion of macro-expressibility: we can’t express effects like state and control. We can define these by translation into continuation-passing style, or macro-express them in terms of a “universal” effect like `gen`

/`yield`

.

What’s next? If you are interested in reading more about…

λ-calculus:

*Lambda Calculus and Combinators: An Introduction*, 2nd ed., Hindley and SeldinDenotational semantics:

*Formal Semantics of Programming Languages*, WinskelTypes: The rest of TAPL

Effects: I’m not aware of a textbook or tutorial introduction; a nice recent paper is “On the expressive power of user-defined effects”, Forster et al.

Compilers:

*Compiling with Continuations*, Appel