A Typed and Unified Reflection for Shift and Shift0

Yui Tamura and Kenichi Asai

July 25, 2026

Agda code for the following paper:

Yui Tamura and Kenichi Asai "A Typed and Unified Reflection for Shift and Shift0," The 28th International Symposium on Principles and Practice of Declarative Programming (PPDP), to appear, 24 pages (August 2026).

Used environments:

Agda 2.8.0, standard library 2.3

All the files in a zip file (typed version) or a zip file (untyped version).

1 Typed reflection

README_en.md
all.agda all the proofs below

Language definitions and related files

DS.agda DS language
DSK.agda Kernel language
CPS.agda CPS language

Translations between languages

Between DS and CPS
- DS-CPS.agda DS -> CPS transformation (cpsE)
- CPS-DS.agda CPS -> DS transformation (dsE)
Between DS and Kernel
- DS-DSK.agda DS -> Kernel transformation (knE)
- DSK-DS.agda Kernel -> DS transformation (embE)
Between Kernel and CPS
- DSK-CPS.agda Kernel -> CPS transformation (cpskE)
- CPS-DSK.agda CPS -> Kernel transformation (dskE)

Proofs

Auxiliary definitions and theorems
- Extensionality.agda axiom of function extensionality
- TypeIsos.agda definitions and proofs of type isomorphisms for each language
Reflection (1)
- Reflect1.agda DS - CPS (composed)
  - Reflect1a.agda DS - Kernel
  - Reflect1b.agda Kernel - CPS
- Reflect1Direct.agda DS - CPS (direct)
Reflection (2)
- Reflect2.agda DS - CPS (composed)
  - Reflect2a.agda Kernel - CPS
  - Reflect2b.agda DS - Kernel
- Reflect2Direct.agda DS - CPS (direct)
Reflection (3)
- Reflect3.agda DS - CPS (composed)
  - Reflect3a.agda DS - Kernel
  - Reflect3b.agda Kernel - CPS
- Reflect3Direct.agda DS - CPS (direct)
Reflection (4)
- Reflect4.agda CPS - DS (composed)
  - Reflect4a.agda CPS - Kernel
  - Reflect4b.agda Kernel - DS
- Reflect4Direct.agda CPS - DS (direct)

2 Untyped reflection

Obtained by stripping off all the type information from the typed version.

README_en.md
all.agda all the proofs below

Language definitions and related files

DS.agda DS language
DSK.agda Kernel language
CPS.agda CPS language

Translations between languages

Between DS and CPS
- DS-CPS.agda DS -> CPS transformation (cpsE)
- CPS-DS.agda CPS -> DS transformation (dsE)
Between DS and Kernel
- DS-DSK.agda DS -> Kernel transformation (knE)
- DSK-DS.agda Kernel -> DS transformation (embE)
Between Kernel and CPS
- DSK-CPS.agda Kernel -> CPS transformation (cpskE)
- CPS-DSK.agda CPS -> Kernel transformation (dskE)

Proofs

Auxiliary definitions and theorems
- Extensionality.agda axiom of function extensionality
- TypeIsos.agda definitions and proofs of type isomorphisms for each language
Reflection (1)
- Reflect1.agda DS - CPS (composed)
  - Reflect1a.agda DS - Kernel
  - Reflect1b.agda Kernel - CPS
- Reflect1Direct.agda DS - CPS (direct)
Reflection (2)
- Reflect2.agda DS - CPS (composed)
  - Reflect2a.agda Kernel - CPS
  - Reflect2b.agda DS - Kernel
- Reflect2Direct.agda DS - CPS (direct)
Reflection (3)
- Reflect3.agda DS - CPS (composed)
  - Reflect3a.agda DS - Kernel
  - Reflect3b.agda Kernel - CPS
- Reflect3Direct.agda DS - CPS (direct)
Reflection (4)
- Reflect4.agda CPS - DS (composed)
  - Reflect4a.agda CPS - Kernel
  - Reflect4b.agda Kernel - DS
- Reflect4Direct.agda CPS - DS (direct)

This document was translated from L^AT_EX by H^EV^EA.