Temporal refinements for Call-By-Push-Value with fixpoint
summary
Proposes temporal refinements for a Call-By-Push-Value calculus with arbitrary fixpoints and shows how a comonadic modality (a box) plus a later modality expresses safety and liveness in a mu‑calculus fragment, lets one prove productivity of non-guarded functions like filter under “always eventually” hypotheses, and gives semantics via domains vs sets (Scott topology issue). Shows an obstruction to a single adjoint (strict vs non‑strict functions) and resolves it by splitting CPO categories and lifting the adjunction to hyperdoctrines; work in progress but the semantic plan is detailed.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 4:59Refinement types
- 9:01Safety and liveness
- 16:58Fixpoints and Scott induction
- 22:58Domain theory limits
- 24:48Polarized CBPV solution
related talks
14mRecovering Purity with Comonads and Capabilities
01h 07mAn introduction to synthetic guarded domain theory with applications to probabilistic(…)
14mAdequacy for Algebraic Effects Revisited
20mModal Mu-Calculus for Free in Agda
13mComputation Focusing
17mNotions of Stack-manipulating Computation and Relative Monads
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...
25mFormalizing pi-Calculus in Guarded Cubical Agda