Compilation

How to go from lambda-calculus and other well-specified functional languages to efficient machine code? This lecture will introduce the main ingredients for achieving this result and proving the correctness of compilation schemes:

• Closures
• Abstract machines
• Explicit substitutions
• Native-code optimizations
• Strong reduction (if time permits).