Normal-order syntax-rules and proving the fix-point of call/cc
10 hours ago
- #call/cc
- #Scheme
- #lambda-calculus
- The talk discusses applications of call/cc and hygienic Scheme macros, including their use as a proof assistant for lambda-calculations.
- Key topics include undelimited and delimited continuations, continuation-passing style (CPS) transforms, and beta-normalization.
- The presentation highlights the influence of Dan Friedman on these topics, developed in response to his challenges.
- A theorem is presented showing equivalence of certain expressions involving call/cc and self-application under CPS transform.
- The talk includes practical examples and lemmas to demonstrate the theorem, using Scheme's macro system for proofs.
- A lambda-calculator is introduced as a source-to-source transformer, emphasizing its simplicity and integration with normalization.
- The presentation concludes with examples of factorial computation using call/cc and discussions on delimited continuations.