Delimited-Control Operators shift0/dollar:

• Thesis: A Fine-Grained Evaluation Strategy for Delimited-Control Operators shift0/dollar
• Contribution:
  • Formalise λ$ calculus with its evaluation strategy
  • Introduce an evaluation strategy for λc$ (a fine-grained version of λ$)
  • Define similarity relations to prove correspondance between both calculi in a form of simulations which state that: similar terms compute to similar values
• Files:
  • λ$ calculus (paper reference: section 2.2)
  • λc$ calculus: a Fine-Grained version of λ$ (paper reference: Figure 1)
  • Correspondence between λ$ and λc$:
    • Simulation: λ$ to λc$
    • Simulation: λc$ to λ$

Makefile generated by coq_makefile -f _CoqProject *.v -o Makefile

---

This is an archived sub-repository of lambda-formalizations that hosts the formalisation code of my thesis.