Operational Algorithmic Game Semantics

on YouTube ↗21m

" summary

Builds a fully abstract trace model for a call-by-push-value calculus with first-order state as a labelled transition system, then refines it (via name schemes and two recycling schemes for indices) into a deterministic visibly pushdown automaton for a defined PTR fragment. Consequences: contextual equivalence becomes decidable, terms in canonical form are checkable in exponential time, and a further restricted fragment yields finite-state automata. Also provides fully abstract translations of IA and RML into the calculus.

AI-written summary · about

" chapters (14)

1. 0:00Operational game semantics intro
2. 1:04Call-by-push-value calculus
3. 3:13Contextual equivalence basics
4. 5:19Game semantics with LTS
5. 8:55Full abstraction via trace equality
6. 9:36Finite trace presentation
7. 11:26Faithful renaming marks
8. 12:54Finite state recycling
9. 14:37Visibly pushdown automata
10. 15:20PTR fragment restrictions
11. 16:23Translations from idealized langs
12. 17:27Deterministic automata cases
13. 17:48Conclusion and future
14. 18:39Questions and answers session