Proofs on different evaluation strategies on pure lambda calculus, the theorem includes: diamond property, adequacy of reduction, and etc…
- Call By Value
- Call By Push Value
Also check out the writeup.
erupmi/cbpv-standardization-proof
The Standardization proof on Call by Value and Call by Push Value Lambda-Calculus
Coq