AndrasKovacs/staged

Staged compilation with dependent types

staged

Staged compilation with two-level type theory.

• ICFP 2024 paper. Code supplement.
• ICFP 2022 paper. Includes a proof of correctness of staging. Appendix. 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