Lambda Calculi Formalizations

Simply Typed Lambda Calculus
- Term representation using Nested Datatypes
  - Progress and Preservation
- Legacy: Type-Level de Bruijn indices (unnecessarily difficult approach)
Delimited-Control Operators shift0/dollar:
- Introduction : Delimited Control
- Contribution:
  - Formalize λ$ 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
- λ$ 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 λ$

Create Makefile with coq_makefile -f _CoqProject *.v -o Makefile

Future Work

Examine the potential of supporting the control0 operator for the current evaluation strategy
Develop the alternative evaluation strategy - the hybrid (reduces differently when under the delimiter) one that aggressively duplicates $
- Simplify both calculi to the most common format to showcase the fine-grained difference - single term-tree tm A, two different reductions
- Remove call-by-value nature from both, let let-bindings do the rest
- Explore a different similarity relation strategy - instead of substituting similar terms try to work on common skeletons (tm A) with a substitution (A → val) of similar values