Run-Time Code Generation
• �A — generator for code of type A
• Modal restrictions guarantee that source
expression will be available at run-time
• [Davies & Pfenning ‘96, ‘00, ‘01]
• Implementation via lightweight generating
extensions
• [Leone & Lee ‘96]
• [Wickline, Lee, Pfenning, Davies ‘98]