# shift0-reflection

Formalization of "Reflection in typed languages with shift and shift0"

- Language definitions and related files
  - `DS.agda`: DS language
  - `DSK.agda`: DSKernel 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 DSKernel
    - `DS-DSK.agda`: DS -> DSKernel transformation (knE)
    - `DSK-DS.agda`: DSKernel -> DS embedding (embE)
  - Between DSKernel and CPS
    - `DSK-CPS.agda`: DSKernel -> CPS transformation (cpskE)
    - `CPS-DSK.agda`: CPS -> DSKernel 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 - DSKernel
      - `Reflect1b.agda`: DSKernel - CPS
    - `Reflect1Direct.agda`: DS - CPS (direct)
  - Reflection (2)
    - `Reflect2.agda`: DS - CPS (composed)
      - `Reflect2a.agda`: DSKernel - CPS
      - `Reflect2b.agda`: DS - DSKernel
    - `Reflect2Direct.agda`: DS - CPS (direct)
  - Reflection (3)
    - `Reflect3.agda`: DS -> CPS (composed)
      - `Reflect3a.agda`: DS -> DSKernel
      - `Reflect3b.agda`: DSKernel -> CPS
    - `Reflect3Direct.agda`: DS -> CPS (direct)
  - Reflection (4)
    - `Reflect4.agda`: CPS -> DS (composed)
      - `Reflect4a.agda`: CPS -> DSKernel
      - `Reflect4b.agda`: DSKernel -> DS
    - `Reflect4Direct.agda`: CPS -> DS (direct)