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. © Elsevier Ltd.
Moggi, E. (1997). A categorical account of two-level languages. In Electronic Notes in Theoretical Computer Science (Vol. 6, p. 272). https://doi.org/10.1016/S1571-0661(05)80155-0