A categorical account of two-level languages
Eugenio Moggi · Electronic Notes in Theoretical Computer Science · 1997
We give an account of two-level languages in terms of indexed categories and universal properties well-known in the context of categorical logic. This account provides three important insights: establishes precise analogies between two-level languages and module languages, explains the two-level languages used in partial evaluation in terms of those used for code generation, suggests extensions that should be valuable for type-specialization and shape-analysis.