A Historical Perspective on Program Transformation and Recent Developments (Invi...
summary
Historical survey ties classic transformation techniques to concrete outcomes: rule-based unfolding/folding rules plus strategies produce a linear-time Fibonacci from an exponential specification by inventing a 2-component tuple (tupling) with a provable theorem that at least two unfolds are needed; allowing multiplication yields logarithmic-time via 2x2 matrix exponentiation; circular Tower of Hanoi uses a cut of breadth six while unbounded breadth forces a stack; transformations synthesize tail‑recursive reverse via lambda abstraction and verify properties (Yale shooting, n‑queens, a^n b^n complement) with transformation‑based model checking.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:52Program correctness and efficiency 1980s
- 3:22Schema transformation techniques
- 4:49Rules and strategies in transformation
- 9:31Fibonacci complexity reduction
- 14:34Nonlinear recurrences generalization
- 19:38Inverse partial evaluation
- 24:05Logic programming specs
- 26:33Theorem proving with transformation
- 30:10Contract verification and model checking
- 31:35Questions and closing remarks
related talks
01h 05mFrom meta frameworks and transformations to distributed computing and more
56mOn Type-Based Techniques for Program Manipulation
37mA Tour of Program Optimization
28mType-directed Program Transformation for Constant-Time Enforcement
01h 28mTutorial on Program Transformations
01h 07mBack to the Future: A Fresh Look at Linear Temporal Logic
59mPrinciples of Programming Language Translators
14mAchieving High-Performance the Functional Way - A Functional Pearl on Expressing High...