- (slides/video) Feeley, 90 minute Scheme to C compiler; (slides) Leroy, Compiling functional languages; the MinCaml compiler
- (code) Bauer, The PL Zoo
- Steele, RABBIT: a compiler for Scheme
- Kennedy, Compiling with Continuations, Continued
- Marlow, How to make a fast curry: push/enter vs eval/apply
- Landin, Call-by-name, call-by-value, and the Lambda-calculus
- "Relating System F and λ2: A Case Study in Coq, Abella and Beluga"
- "Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)"
- "My first fifteen compilers"
- "Compiling to Categories"
- "A first-order one-pass CPS transformation" (also at http://www.brics.dk/RS/01/49/BRICS-RS-01-49.ps.gz)
- "How to prove a compiler fully abstract"
- Verified Transformations on Functional Programs Using the Higher-Order Abstract Syntax Approach
- (Thesis) Verified Compilation of Functional Programs
- From System F to Typed Assembly Language