staged

Staged compilation with two-level type theory.

This is a system for two-stage compilation with full dependent types at both stages; as far as I know, the first such system.

• Preprint. Includes a proof of correctness of staging.
• Demo implementation, together with a tutorial and some code examples. Has an efficient staging implementation and powerful inference for stage annotations.

Older material, somewhat obsolete now:

• Abstract at the TYPES 2021 conference.
• Slightly longer abstract, discussing generativity.
• Videos:
  • https://www.youtube.com/watch?v=ove4TQsXemY
  • https://www.youtube.com/watch?v=WOd0ZFbJfQg
  • https://www.youtube.com/watch?v=ai4vU1Naopk