Course pages 2018–19
Metaprogramming
Tentative lecture schedule
- Thursday 4 October 2018 (11am, FW26)
- Introduction; programs as data, data as programs
Nada Amin
Slides (errata)
- Tuesday 9 October 2018 (11am, FW26)
- Interpreters
Nada Amin
- Thursday 11 October 2018 (11am, FW26)
- Reification and reflection
Nada Amin
Slides
- Tuesday 16 October 2018 (11am, FW26)
- Reification and reflection
Nada Amin
- Thursday 18 October 2018 (11am, FW26)
- Practical session
Nada Amin
- Tuesday 23 October 2018 (11am, FW26)
- Code generation: Futamura projections, LMS, generative programming, verification
Nada Amin
Slides
Code (regular expressions) - Thursday 25 October 2018 (11am, FW26)
- Code generation: Futamura projections, LMS, generative programming, verification (continued)
Nada Amin
Slides
Code (regular expressions) - Tuesday 30 October 2018 (11am, FW26)
- Tagless Embedded DSLs
Jeremy Yallop
Slides
Code from the lectures
- Thursday 1 November 2018 (11am, FW26)
- Staging with quotation
Jeremy Yallop
Slides
- Tuesday 6 November 2018 (11am, FW26)
- Practical session
Jeremy Yallop
- Thursday 8 November 2018 (11am, FW26)
- From interpreters to compilers
Timothy Griffin
Background: Call-by-name, call-by-value and the λ-calculus (Plotkin, 1975)
Background: Defunctionalization at Work (Danvy & Nielsen, 2001)
Background: From Interpreter to Compiler and Virtual Machine: A Functional Derivation (Ager et al., 2003)
- Tuesday 13 November 2018 (11am, FW26)
- From interpreters to compilers (continued)
Timothy Griffin
- Thursday 15 November 2018 (11am, FW26)
- From interpreters to compilers (concluded)
Timothy Griffin
deep_embedding_v1.ml
- Tuesday 20 November 2018 (11am, FW26)
- Practical session
Jeremy Yallop
- Thursday 22 November 2018 (11am, FW26)
- Practical session
Jeremy Yallop
- Tuesday 27 November 2018 (11am, FW26)
- Reflection for proofs in F*
Jonathan Protzenko