Reasoning about Staged Programs
• Developed type theory for reasoning about
staged programs [Pfenning’01]
• Enabled by clean and minimal design
• Required formalization of “dead code”