Computation Focusing
summary
Presents a focused polymorphic call-by-push-value calculus and proves computational completeness: every well-typed term has a βη-equivalent focused representative, cutting the search from all contexts to only focused contexts. Uses focused typing rules as a normalization/restriction tool to prove contextual equivalences (including an existential-type example that logical relations struggle with) and establishes full abstraction for a compiler from a pure total CBPV into a language with divergence and simple effect types.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:24Reasoning About Programs
- 1:05Syntactic Proofs of Contextual Equivalence
- 2:11An Existential Example
- 3:50Overview: Computation Focusing
- 4:39Focusing Example
- 6:24Properties of Focused Terms
- 7:18Focusing and Contextual Equivalence
- 7:46A Context Lemma
- 8:12Return to the Existential Example
- 10:03Compiler Correctness
related talks
45mA categorical view of computational effects
17mNotions of Stack-manipulating Computation and Relative Monads
26mTemporal refinements for Call-By-Push-Value with fixpoint
22mMoebius: Metaprogramming using Contextual Types
46mThe Calculated Typer (Functional Pearl)
15mMonadic Compiler Calculation (Functional Pearl)
12mTowards Dependently-Typed Control Effects (Extended Abstract)
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)